# 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)).