AXIOMS OF SET THEORY

Axiom ZF1 - Extensionality.
If x and y are sets then x = y <=> ( /\(z) z:-x <=> z:-y ).

Axiom ZF2 - Empty set.
There exists a set y such that /\(x) !(x:-y).

Definition S.A.0
We define that O = y if and only if /\(x) !(x:-y).

This definition is correct because y is unique by Axiom ZF1.

Axiom ZF3 - Unordered pairs.
If x,y are sets then there exists a set z such that
/\(a) (a:-z <=> (a = x or a = y)).

Definition S.A.1
Let x,y be sets.
We define that
{x,y} = z if and only if /\(a) (a:-z <=> (a = x or a = y)).
We define that {x} = {x,x}.

This definition is correct because z is unique by Axiom ZF1. 

Axiom ZF4 - Selection.
If z,y1,y2, ..., yn are sets and P is a well-formed formula
containing variables 'y1', 'y2', ..., 'yn' and a free variable 'x'
and doesn't contain other free variables then 
there exits a set y such that
/\(x) ( x:-y <=> (x:-z and P) ).

Definition S.A.2
Let z,y1, ...,yn be sets and let P be a well-formed formula as above.
We define that 
{x:-z | P} = y if and only if /\(x) ( x:-y <=> (x:-z and P) ).

This definition is correct because y is unique by Axiom ZF1.

Remark: Compare with Definition S.C.15.

Axiom ZF5 - Union.
If x is a set then there exists a set y such that /\(a) 
( a:-y <=> (\/(z) z:-x and a:-z) ).

Definition S.A.3
Let x be a set.
We define that 
u(x) = y if and only if /\(a) ( a:-y <=> (\/(z) z:-x and a:-z) ).

This definition is correct because y is unique by Axiom ZF1.

Axiom ZF6 - Power set.
If x is a set then there exists a set z such that 
/\(y)( y:-z <=> ( /\(a) (a:-y => a:-x) ) ).

Axiom ZF7 - Infinity.
There exists a set m such that O:-m and /\(x) (x:-m => u({x,{x}}):-m).

Axiom ZF9 - Regularity.
If x is a set and x != O then \/(y) (y:-x and /\(a) !(a:-x and a:-y)).