Module Type ZF.

Parameter set : Type.
Parameter IN : set → set → Prop.
Definition nIN (x y:set) : Prop := ¬IN x y.
Infix "∈" := IN (at level 70).
Infix "∉" := nIN (at level 70).

Definition Subq (X Y:set) : Prop := ∀ z, z ∈ X → z ∈ Y.
Infix "⊆" := Subq (at level 70).

(*** Extensionality ***)
Axiom set_ext : ∀ X Y, X ⊆ Y → Y ⊆ X → X = Y.

(*** Epsilon Induction (Foundation) ***)
Axiom eps_ind : ∀ (P:set → Prop), (∀ X, (∀ x, x ∈ X → P x) → P X) → ∀ X, P X.

(*** Empty ***)
Parameter empty : set.
Notation "∅" := empty.
Axiom emptyE : ∀ (x:set), x ∉ ∅.

(*** Unordered Pairs ***)
Parameter upair : set → set → set.
Notation "{ x , y }" := (upair x y).
Axiom upairAx : ∀ (x y z:set), z ∈ {x,y} ↔ z = x ∨ z = y.

(*** Unions ***)
Parameter union : set → set.
Notation "⋃" := union (at level 40).
Axiom unionAx : ∀ (x z:set), z ∈ ⋃ x ↔ ∃ y, y ∈ x ∧ z ∈ y.

(*** Power Sets ***)
Parameter power : set → set.
Notation "℘" := power.
Axiom powerAx : ∀ (X:set), ∀ Y:set, Y ⊆ X ↔ Y ∈ ℘ X.

(*** Replacement (for functions) ***)
Parameter repl : set → (set → set) → set.
Notation "{ f | x ⋳ X }" := (repl X (fun x:set ⇒ f)).
Axiom replAx : ∀ X f z, z ∈ {f x|x ⋳ X} ↔ ∃ x, x ∈ X ∧ z = f x.

(*** Separation ***)
Parameter sep : set → (set → Prop) → set.
Notation "{ x ⋳ X | P }" := (sep X (fun x:set ⇒ P)).
Axiom sepAx : ∀ X P z, z ∈ {x ⋳ X|P x} ↔ z ∈ X ∧ P z.

(*** singleton definition ***)
Definition sing : set → set := fun x ⇒ {x,x}.

(*** binunion definition ***)
Definition binunion (X Y:set) := ⋃ {X,Y}.

(*** Infinity ***)
Axiom infinity : ∃ X:set, ∅ ∈ X ∧ (∀ x, x ∈ X → binunion x (sing x) ∈ X).

End ZF.