Zermelo-Fraenkel Set Theory

∀u∈x(φ(u))     ⇔   ∀u(u∈x⇒φ(u))
∃u∈x(φ(u))     ⇔   ∃u(u∈x∧φ(u))
z={u:φ(u)}     ⇔   ∀u(u∈z⇔φ(u))
z={u∈x:φ(u)}   ⇔   z={u:u∈x∧φ(u)}
z⊂x            ⇔   ∀y∈z(y∈x)
∀u⊂x(φ(u))     ⇔   ∀u(u⊂x⇒φ(u))
∃u⊂x(φ(u))     ⇔   ∃u(u⊂x∧φ(u))
z=P(x)         ⇔   ∀u(u⊂x⇔u∈z)
z={u⊂x:φ(u)}   ⇔   z={u∈P(x):φ(x)}
z=Ux           ⇔   ∀u(∃v∈x(v∈w)⇔u∈z)
z=∩x           ⇔   ∀u(∀v∈x(v∈w)⇔u∈z)
z=x-y          ⇔   {u∈x:u∉y}
z={x,y}        ⇔   x∈z∧y∈z∧∀w(w∈z⇒(x=w∨y=w))
z={x}          ⇔   z={x,x}
z=(x,y)        ⇔   z={{x},{x,y}}
z=x∪y          ⇔   z=∪{x,y}
z=x∩y          ⇔   x-(x-y)
z=a×b          ⇔   {(x,y):x∈a∧y∈b}
z=∅            ⇔   ¬∃x(x∈z)
z=S(x)         ⇔   z=x∪{x}
z⊃ω            ⇔   ∅∈z∧∀x∈z(S(x)∈z)
z=ω            ⇔   z⊃ω∧∀x(x⊃ω⇒x⊃z)
z∈Trans        ⇔   ∀x∈z(x⊂z)
z=tc(x)        ⇔   z∈Trans∧x∈z∧∀y(y∈Trans∧x∈y⇒z⊂y)
z∈Reg          ⇔   z=∅∨∃x∈z(x∩z=∅)
z∈WF[∈]	       ⇔   ∀y⊂tc(x)(y≠∅⇒∃z∈y∀w∈y(z∉w)



α∈Ord          ⇔   α∈Trans∧α∈WF[∈]∧∀β∈α()
α∈Succ         ⇔   α∈Ord∧∃β(α=S(β))
α∈Lim          ⇔   α≠∅∧α∈Ord∧α∉Succ
α∈ℕ            ⇔   α=∅∨∀β∈α(β∈Succ)

AXIOMS:

I. Extensionality:
∀x∀y(∀z(z∈x⇔z∈y)⇒x=y)

II. Foundation:
∀x(x∈Reg)

III. Separation:
∀x∃y(y={u∈x:φ(u))   (x does not occur in φ)

IV. Pairing:
∀x∀y∃z(z={x,y})

V. Union:
∀x∃y(y=∪x)

VI. Powerset:
∀x∃y(y=P(x))

VII. Infinity:
∃x(x=ω)

VIII. Choice:
∀x(∀y∈x∀z∈x(x≠∅∧x∩y=∅)⇒∃w∀y∈x∃z∈y(w∩y={z}))

IX. Replacement:
∀p∀A(∀x∈A∀y∀z(φ(x,y,p)∧φ(x,z,p)⇒y=z)⇒∃z∀y(y∈z⇔∃x∈A(φ(x,y,p)))    (B does not occur in φ)