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.