Axioms of Set Theory

S0: Axiom of The Empty Set

∃y{∀x[¬(x ∈ y)]}

S1: Axiom of Extensionality

∀A{∀B[∀x(x ∈ A ⇔ x ∈ B) ⇔ ∀y(A ∈ y ⇔ B ∈ y)]}

S2: Axiom of Pairing

∀A{∀B[∃C(∀x{x ∈ C ⇔ [x = A ∨ x = B]})]}

S3: Axiom of The Power Set

∀A{∃P[∀S(S ∈ P ⇔ S ⊆ A)]}

S4: Axiom Schema of Separation

∀A{∃S[∀x(x ∈ S ⇔ [x ∈ A ∧ P])]}

S5: Axiom of Union

∀F{∃U[∀x(x ∈ U ⇔ ∃S[S ∈ F ∧ x ∈ S])]}

S6: Axiom of Infinity

∃H{Ø ∈ H ∧ ∀C(C ∈ H ⇒ [(C ∪ {C}) ∈ H])}

S7: Axiom of Choice

For each set F of non-empty sets [¬(A = Ø) for each A ∈ F] , there is a "choice" function        f : F → ∪F with F(A) ∈ A for each A ∈ F.