Module Type ZF.

Parameter set : Type.
Parameter IN : setsetProp.
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 Xz Y.
Infix "⊆" := Subq (at level 70).

(*** Extensionality ***)
Axiom set_ext : X Y, X YY XX = Y.

(*** Epsilon Induction (Foundation) ***)
Axiom eps_ind : (P:setProp), ( X, ( x, x XP x) → P X) → X, P X.

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

(*** Unordered Pairs ***)
Parameter upair : setsetset.
Notation "{ x , y }" := (upair x y).
Axiom upairAx : (x y z:set), z {x,y} z = x z = y.

(*** Unions ***)
Parameter union : setset.
Notation "⋃" := union (at level 40).
Axiom unionAx : (x z:set), z x y, y x z y.

(*** Power Sets ***)
Parameter power : setset.
Notation "℘" := power.
Axiom powerAx : (X:set), Y:set, Y X Y X.

(*** Replacement (for functions) ***)
Parameter repl : set → (setset) → set.
Notation "{ f | x ⋳ X }" := (repl X (fun x:setf)).
Axiom replAx : X f z, z {f x|x X} x, x X z = f x.

(*** Separation ***)
Parameter sep : set → (setProp) → set.
Notation "{ x ⋳ X | P }" := (sep X (fun x:setP)).
Axiom sepAx : X P z, z {x X|P x} z X P z.

(*** singleton definition ***)
Definition sing : setset := fun x{x,x}.

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

(*** Infinity ***)
Axiom infinity : X:set, X ( x, x Xbinunion x (sing x) X).

End ZF.