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 := forall z, z ∈ X -> z ∈ Y. Infix "⊆" := Subq (at level 70). (*** Extensionality ***) Axiom set_ext : forall X Y, X ⊆ Y -> Y ⊆ X -> X = Y. (*** Epsilon Induction (Foundation) ***) Axiom eps_ind : forall (P:set -> Prop), (forall X, (forall x, x ∈ X -> P x) -> P X) -> forall X, P X. (*** Empty ***) Parameter empty : set. Notation "∅" := empty. Axiom emptyE : forall (x:set), x ∉ ∅. (*** Unordered Pairs ***) Parameter upair : set -> set -> set. Notation "{ x , y }" := (upair x y). Axiom upairAx : forall (x y z:set), z ∈ {x,y} <-> z = x \/ z = y. (*** Unions ***) Parameter union : set -> set. Notation "⋃" := union (at level 40). Axiom unionAx : forall (x z:set), z ∈ ⋃ x <-> exists y, y ∈ x /\ z ∈ y. (*** Power Sets ***) Parameter power : set -> set. Notation "℘" := power. Axiom powerAx : forall (X:set), forall 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 : forall X f z, z ∈ {f x|x ⋳ X} <-> exists 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 : forall 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 : exists X:set, ∅ ∈ X /\ (forall x, x ∈ X -> binunion x (sing x) ∈ X). End ZF.