diff --git a/ZFLean/Def.lean b/ZFLean/Def.lean
index 0ed8f92..85c4482 100644
--- a/ZFLean/Def.lean
+++ b/ZFLean/Def.lean
@@ -120,6 +120,13 @@ private lemma some_inf_mem_sep_inductive_set : some_inf ∈ some_inf.powerset.se
   simp only [mem_sep, mem_powerset, subset_refl, true_and]
   exact inductive_some_inf
 
+theorem sdiff_subset {s t : ZFSet} : s \ t ⊆ s := by
+  intro x
+  rw [mem_sdiff]
+  rintro ⟨h, _⟩
+  exact h
+
+/-- Symmetric difference of two sets, denoted by `Δ`. -/
 def symmDiff (p q : ZFSet) : ZFSet := (p \ q) ∪ (q \ p)
 infix:70 " Δ " => symmDiff
 
@@ -163,6 +170,80 @@ theorem inter_mono {x y z : ZFSet} :  x ⊆ z → y ⊆ z → x ∩ y ⊆ z := b
   rw [ZFSet.mem_inter] at ha
   exact hx ha.1
 
+
+theorem non_empty_pair {a b : ZFSet} : Nonempty (a.pair b) := by
+  rw [pair]
+  exact ⟨{a}, mem_insert {a} {{a, b}}⟩
+
+def π₁ (x : ZFSet) : ZFSet := ⋃₀ (⋂₀ x)
+
+open Classical in -- couldn't find another way
+noncomputable def π₂ (x : ZFSet) : ZFSet :=
+  let δ : ZFSet := (⋃₀ x \ ⋂₀ x)
+  if δ = ∅ then π₁ x else ⋃₀ δ
+
+@[simp] theorem π₁_pair (x y : ZFSet) : π₁ (x.pair y) = x := by
+  unfold π₁ pair
+  ext
+  rw [sInter_pair, mem_sUnion]
+  constructor
+  · rintro ⟨w, l, r⟩
+    rw [mem_inter, mem_singleton, mem_pair] at l
+    rw [l.1] at r
+    assumption
+  · intro h
+    exists x
+    rw [mem_inter, mem_singleton, mem_pair]
+    exact ⟨⟨rfl, .inl rfl⟩, h⟩
+
+@[simp] theorem pair_inter {x y : ZFSet} : {x} ∩ {x, y} = ({x} : ZFSet) := by
+    ext
+    rw [mem_inter, mem_singleton, mem_pair]
+    constructor
+    · rintro ⟨rfl, _ | rfl⟩ <;> rfl
+    · rintro rfl
+      exact ⟨rfl, .inl rfl⟩
+
+@[simp] theorem pair_union {x y : ZFSet} : {x} ∪ {x, y} = ({x, y} : ZFSet) := by
+    ext
+    rw [mem_union, mem_singleton, mem_pair]
+    exact or_self_left
+
+@[simp] theorem pair_minus {x y : ZFSet} : x ≠ y → {x, y} \ {x} = ({y} : ZFSet) := by
+  intro x_ne_y
+  ext z
+  rw [mem_sdiff, mem_pair, mem_singleton, mem_singleton]
+  constructor
+  · rintro ⟨rfl | rfl, r⟩
+    · contradiction
+    · rfl
+  · rintro rfl
+    exact ⟨.inr rfl, x_ne_y ∘ Eq.symm⟩
+
+@[simp] theorem π₂_pair (x y : ZFSet) : π₂ (x.pair y) = y := by
+  unfold π₂
+  dsimp
+  split_ifs with h
+  · rw [π₁_pair]
+    unfold pair at h
+    rw [sUnion_pair, pair_union, sInter_pair, pair_inter] at h
+    rw [ZFSet.ext_iff] at h
+    specialize h y
+    simpa only [mem_sdiff, mem_insert_iff, mem_singleton, eq_self,
+      or_true, true_and, notMem_empty, iff_false, not_not, eq_comm] using h
+  · unfold pair at *
+    rw [sUnion_pair, pair_union, sInter_pair, pair_inter] at h ⊢
+    rw [pair_minus]
+    · exact sUnion_singleton
+    · intro h'
+      rw [h'] at h
+      simp [ZFSet.ext_iff] at h
+
+theorem pair_eta {z A B : ZFSet} (h : z ∈ A.prod B) : z = z.π₁.pair z.π₂ := by
+  rw [mem_prod] at h
+  obtain ⟨a, ha, b, hb, rfl⟩ := h
+  rw [π₁_pair, π₂_pair]
+
 end Preamble
 
 end ZFSet
diff --git a/ZFLean/Functions.lean b/ZFLean/Functions.lean
index 0be619f..0d8413d 100644
--- a/ZFLean/Functions.lean
+++ b/ZFLean/Functions.lean
@@ -5,8 +5,8 @@ Authors: Vincent Trélat
 -/
 module
 
-public import ZFLean.Rationals
 public import ZFLean.Booleans
+public import ZFLean.Naturals
 public import ZFLean.Tactics
 
 /-!
@@ -24,6 +24,86 @@ set_option linter.unusedVariables false
 
 section Relations
 
+/--
+Domain of a (binary) relation. A proof that `f` is a relation is needed and tried to be
+automatically inferred.
+-/
+-- abbrev Dom   (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) :=
+--   ⋃₀ (A.powerset.sep λ 𝒟 => IsFunc 𝒟 B f) --NOTE: this def was specific to functions
+abbrev Dom (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) :=
+  A.sep (fun x => ∃ y ∈ B, x.pair y ∈ f)
+
+abbrev Range (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) :=
+  B.sep (fun y => ∃ x ∈ A, x.pair y ∈ f)
+
+theorem mem_dom_of {f A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) {x y : ZFSet} :
+    x.pair y ∈ f → x ∈ f.Dom hf := by
+  intro h
+  rw [mem_sep]
+  exact ⟨pair_mem_prod.mp (hf h) |>.1, y, pair_mem_prod.mp (hf h) |>.2, h⟩
+
+theorem mem_range_of {f A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) {x y : ZFSet} :
+    x.pair y ∈ f → y ∈ f.Range hf := by
+  intro h
+  rw [mem_sep]
+  exact ⟨pair_mem_prod.mp (hf h) |>.2, x, pair_mem_prod.mp (hf h) |>.1, h⟩
+
+theorem mem_dom_iff {f A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) {x : ZFSet} :
+    x ∈ f.Dom hf ↔ ∃ y, x.pair y ∈ f := by
+  rw [mem_sep, and_iff_right_of_imp]
+  conv =>
+    enter [1,1,y]
+    rw [and_iff_right_of_imp]
+    · skip
+    · tactic =>
+        intro h
+        apply mem_range_of hf at h
+        apply sep_subset at h
+        exact h
+  rintro ⟨_, _, h⟩
+  apply mem_dom_of hf at h
+  apply sep_subset at h
+  exact h
+
+theorem mem_range_iff {f A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) {y : ZFSet} :
+    y ∈ f.Range hf ↔ ∃ x, pair x y ∈ f := by
+  rw [mem_sep, and_iff_right_of_imp]
+  conv =>
+    enter [1,1,y]
+    rw [and_iff_right_of_imp]
+    · skip
+    · tactic =>
+        intro h
+        apply mem_dom_of hf at h
+        apply sep_subset at h
+        exact h
+  rintro ⟨_, _, h⟩
+  apply mem_range_of hf at h
+  apply sep_subset at h
+  exact h
+
+theorem dom_subset (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) : f.Dom ⊆ A :=
+  sep_subset
+
+theorem range_subset (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) : f.Range ⊆ B :=
+  sep_subset
+
+theorem is_rel_ext_iff {A B C D : ZFSet} (R S : ZFSet)
+  (hR : R ⊆ A.prod B := by zrel) (hS : S ⊆ C.prod D := by zrel) :
+    (∀ x y : ZFSet, x.pair y ∈ R ↔ x.pair y ∈ S) ↔ R = S := by
+  constructor
+  · intro h
+    ext z
+    constructor
+    · intro z_R
+      obtain ⟨x, _, y, _, rfl⟩ := mem_prod.mp <| hR z_R
+      exact (h x y).mp z_R
+    · intro z_S
+      obtain ⟨x, _, y, _, rfl⟩ := mem_prod.mp <| hS z_S
+      exact (h x y).mpr z_S
+  · intro rfl x y
+    trivial
+
 -- syntax "zrel" : tactic
 -- macro_rules | `(tactic| zrel) => `(tactic| (
 --   change ?R ⊆ ZFSet.prod ?A ?B
@@ -61,10 +141,7 @@ theorem mem_inv {x y R A B : ZFSet} (hR : R ⊆ A.prod B) :
     · exact h
 
 @[zrel]
-theorem subset_prod_inv {R A B : ZFSet} (hR : R ⊆ A.prod B) : R⁻¹ ⊆ B.prod A := by
-  intro z hz
-  rw [inv, mem_sep] at hz
-  exact hz.1
+theorem subset_prod_inv {R A B : ZFSet} (hR : R ⊆ A.prod B) : R⁻¹ ⊆ B.prod A := sep_subset
 
 -- macro_rules | `(tactic| zrel) => `(tactic| apply subset_prod_inv; done)
 
@@ -78,17 +155,25 @@ theorem inv_involutive {R A B : ZFSet} (hR : R ⊆ A.prod B) : (R⁻¹)⁻¹ = R
     obtain ⟨a, ha, b, hb, rfl⟩ := hR h |> mem_prod.mp
     rwa [mem_inv, mem_inv]
 
-/--
-Domain of a (binary) relation. A proof that `f` is a relation is needed and tried to be
-automatically inferred.
--/
--- abbrev Dom   (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) :=
---   ⋃₀ (A.powerset.sep λ 𝒟 => IsFunc 𝒟 B f) --NOTE: this def was specific to functions
-abbrev Dom (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) :=
-  A.sep (fun x => ∃ y ∈ B, pair x y ∈ f)
+theorem dom_inv (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) :
+    Dom f⁻¹ = Range f := by
+  ext z
+  rw [mem_dom_iff, mem_range_iff]
+  conv => enter [1, 1, y] ; rw [mem_inv]
 
-abbrev Range (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) :=
-  B.sep (fun y => ∃ x ∈ Dom f hf, pair x y ∈ f)
+theorem range_inv (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) :
+    Range f⁻¹ = Dom f := by
+  ext z
+  rw [mem_dom_iff, mem_range_iff]
+  conv => enter [1, 1, y] ; rw [mem_inv]
+
+def is_rel_symmetric (f : ZFSet) {A B : ZFSet} (hf : f ⊆ A.prod B := by zrel) :=
+  f = f⁻¹
+
+theorem is_rel_symmetric_iff (R : ZFSet) {A B : ZFSet} (hR : R ⊆ A.prod B := by zrel) :
+    is_rel_symmetric R hR ↔ ∀ x y : ZFSet, x.pair y ∈ R ↔ y.pair x ∈ R := by
+  rw [is_rel_symmetric, ←is_rel_ext_iff R R⁻¹ hR (subset_prod_inv hR)]
+  conv => enter [1, x, y] ; rw [mem_inv]
 
 end Relations
 
@@ -224,24 +309,6 @@ theorem is_pfunc_func_exists {f A B : ZFSet} :
       exact ⟨y, pair, fun z hz ↦ func x z hz y pair⟩
     repeat (intro z hz; exact mem_sep.mp hz |>.left)
 
-theorem pfun_dom_subset (f : ZFSet) {A B} (hf : f.IsPFunc A B) : f.Dom ⊆ A := by
-  rintro x x_dom
-  rw [mem_sep] at x_dom
-  exact x_dom.1
-
-theorem mem_dom {f A B : ZFSet} (hf : f.IsPFunc A B) {x y : ZFSet} :
-    pair x y ∈ f → x ∈ f.Dom := by classical
-  intro mem_pair
-  obtain ⟨D, C, is_func_DC, Dsub, Csub⟩ := is_pfunc_func_exists hf
-  rcases hf with ⟨sub, unique⟩
-  obtain ⟨a, ha, b, hb, eq⟩ := mem_prod.mp <| sub mem_pair
-  rw [pair_inj] at eq
-  rcases eq with ⟨rfl, rfl⟩
-  rw [mem_sep]
-  and_intros
-  · exact ha
-  · use y
-
 theorem is_func_dom_range (f : ZFSet) {A B} (hf : f.IsPFunc A B) :
     IsFunc f.Dom f.Range f := by
   classical
@@ -260,9 +327,6 @@ theorem is_func_dom_range (f : ZFSet) {A B} (hf : f.IsPFunc A B) :
       and_intros
       · exact b_B
       · exists a
-        and_intros
-        · exact mem_dom ⟨sub, unique⟩ h
-        · exact h
   · intro z z_dom
     rw [mem_sep] at z_dom
     obtain ⟨zA, w, hw, zw_f⟩ := z_dom
@@ -409,10 +473,22 @@ theorem range_Id {A : ZFSet} : (𝟙A).Range = A := by
   ext1 z
   simp only [mem_sep, and_iff_left_iff_imp]
   intro hz
-  use z, ⟨hz, ?_⟩
-  · rw [pair_mem_Id_iff hz]
-  · use z, hz
-    rw [pair_mem_Id_iff hz]
+  use z, hz
+  rw [pair_mem_Id_iff hz]
+
+def is_rel_reflexive (R : ZFSet) {A : ZFSet} (hR : R ⊆ A.prod A) := 𝟙A ⊆ R
+
+theorem is_rel_reflexive_iff (R : ZFSet) {A : ZFSet} (hR : R ⊆ A.prod A) :
+    is_rel_reflexive R hR ↔ ∀ x ∈ A, x.pair x ∈ R  := by
+  rw [is_rel_reflexive, subset_def]
+  conv =>
+    enter [1, z]
+    rw [mem_Id_iff]
+  constructor
+  · intro h x x_A
+    exact h ⟨x, x_A, rfl⟩
+  · rintro h _ ⟨x, x_A, rfl⟩
+    exact h x x_A
 
 def IsPermutation (σ E : ZFSet) := ∃ (hσ : E.IsFunc E σ), σ.IsBijective
 
@@ -483,6 +559,10 @@ theorem Id.composition_right {f A B : ZFSet} (hf : f ⊆ A.prod B) : composition
     · obtain ⟨a, aA, b, bB, rfl⟩ := mem_prod.mp <| hf xf
       exists a, b
 
+@[zrel]
+theorem is_rel_of_composition {f g : ZFSet} {A B C : ZFSet} : (composition g f A B C) ⊆ A.prod C :=
+  sep_subset
+
 @[zpfun]
 theorem IsPFunc_of_composition_IsPFunc {f g : ZFSet} {A B C : ZFSet}
   (hf : f.IsPFunc A B) (hg : g.IsPFunc B C) :
@@ -564,6 +644,31 @@ infixl:90 " ∘ᶻ " => fcomp
     · exact hg.1 gwy |> pair_mem_prod.mp |>.2
     · use w
 
+def is_rel_transitive (R : ZFSet) {A B : ZFSet} (hR : R ⊆ A.prod B := by zrel) :=
+  (composition R R A B B) ⊆ R
+
+theorem is_rel_transitive_iff (R : ZFSet) {A B : ZFSet} (hR : R ⊆ A.prod B := by zrel) :
+    is_rel_transitive R hR ↔ ∀ x y z : ZFSet, x.pair y ∈ R ∧ y.pair z ∈ R → x.pair z ∈ R := by
+  rw [is_rel_transitive, subset_def]
+  conv =>
+    enter [1, z]
+    rw [mem_composition]
+  constructor
+  · rintro h x y z ⟨l,r⟩
+    apply h
+    exists x, y, z
+    exact ⟨rfl,
+      dom_subset R hR <| mem_dom_of hR l,
+      range_subset R hR <| mem_range_of hR r,
+      range_subset R hR <| mem_range_of hR l,
+      l, r⟩
+  · rintro h _ ⟨x, y, z, rfl, _, _, _, t⟩
+    exact h x y z t
+
+@[expose]
+def is_rel_equivalence (R : ZFSet) {A : ZFSet} (hR : R ⊆ A.prod A := by zrel) :=
+  R.is_rel_reflexive hR ∧ R.is_rel_symmetric hR ∧ R.is_rel_transitive hR
+
 theorem IsInjective.composition_of_injective {f g : ZFSet} {A B C : ZFSet}
   {hf : A.IsFunc B f} {hg : B.IsFunc C g}
   (finj : f.IsInjective) (ginj : g.IsInjective) :
@@ -688,7 +793,7 @@ A `zdom_conv` seed rather than a `zdom` one: in the main search it would let `so
 loop between `x ∈ A` and `x ∈ f.Dom` (see `ZFLean/Tactics.lean`). -/
 @[zdom_conv]
 theorem mem_of_mem_dom {f A B : ZFSet} (hf : f.IsPFunc A B) {x : ZFSet} (hx : x ∈ f.Dom) : x ∈ A :=
-  pfun_dom_subset f hf hx
+  dom_subset f (is_rel_of_is_pfunc hf) hx
 
 /-- Introduction form of `pair_mem_prod`. -/
 @[zdom]
@@ -777,12 +882,12 @@ theorem IsPFunc.exists_unique_of_mem_dom {f A B : ZFSet}
     exact hf.2 _ _ xy_f _ xy'_f
 
 theorem fapply.of_pair {f A B : ZFSet} (hf : f.IsPFunc A B) {x y : ZFSet} (hxy : x.pair y ∈ f) :
-  @ᶻf ⟨x, mem_dom hf hxy⟩ = ⟨y, And.right <| pair_mem_prod.mp <| hf.1 hxy⟩ := by
+  @ᶻf ⟨x, mem_dom_of (is_rel_of_is_pfunc hf) hxy⟩ = ⟨y, And.right <| pair_mem_prod.mp <| hf.1 hxy⟩ := by
   dsimp [fapply]
   generalize_proofs y_def choose_B yB
   congr
   have spec := Classical.choose_spec y_def |>.2
-  obtain ⟨w, xw, uniq⟩ := IsPFunc.exists_unique_of_mem_dom hf (mem_dom hf hxy)
+  obtain ⟨w, xw, uniq⟩ := IsPFunc.exists_unique_of_mem_dom hf (mem_dom_of (is_rel_of_is_pfunc hf) hxy)
   exact uniq _ hxy ▸ uniq _ spec
 
 theorem IsPFunc.supset_of_range {f A B : ZFSet} (hf : f.IsPFunc A B) : f.Range ⊆ B := by
@@ -790,25 +895,10 @@ theorem IsPFunc.supset_of_range {f A B : ZFSet} (hf : f.IsPFunc A B) : f.Range 
   rw [mem_sep] at y_B
   exact y_B.1
 
-theorem IsPFunc.mem_range_of_mem {f A B : ZFSet}
-  (hf : f.IsPFunc A B) {x y : ZFSet} (hxy : x.pair y ∈ f) :
-    y ∈ f.Range := by
-  rw [mem_sep]
-  and_intros
-  · obtain ⟨_,_,_,_,eq⟩ := mem_prod.mp <| hf.1 hxy
-    rw [pair_inj] at eq
-    rcases eq with ⟨rfl, rfl⟩
-    assumption
-  · exists x
-    and_intros
-    · exact mem_dom hf hxy
-    · exact hxy
-
 theorem IsPFunc.nonempty_range_of_nonempty_dom {f A B x y : ZFSet}
   (hf : f.IsPFunc A B) (hxy : x.pair y ∈ f) :
     f.Range ≠ ∅ := by
-  have x_dom := mem_dom hf hxy
-  have y_dom := mem_range_of_mem hf hxy
+  have y_ran := mem_range_of (is_rel_of_is_pfunc hf) hxy
   rw [nonempty_exists_iff]
   exists y
 
@@ -836,7 +926,7 @@ theorem IsInjective.apply_surj {f A B : ZFSet} (hf : IsFunc A B f) (surj : f.IsS
     Function.Surjective @ᶻf := by
   rintro ⟨y, yB⟩
   obtain ⟨x, -, pair⟩ := surj y yB
-  have x_dom : x ∈ f.Dom := mem_dom (is_func_is_pfunc hf) pair
+  have x_dom : x ∈ f.Dom := mem_dom_of (is_rel_of_is_func hf) pair
   exists ⟨x, x_dom⟩
   exact fapply.of_pair (is_func_is_pfunc hf) pair
 
@@ -845,7 +935,7 @@ theorem IsInjective.apply_surj_pfun {f A B : ZFSet}
     Function.Surjective @ᶻf := by
   rintro ⟨y, yB⟩
   obtain ⟨x, -, pair⟩ := surj y yB
-  have x_dom' : x ∈ f.Dom := mem_dom hf pair
+  have x_dom' : x ∈ f.Dom := mem_dom_of (is_rel_of_is_pfunc hf) pair
   exists ⟨x, x_dom'⟩
   exact fapply.of_pair hf pair
 
@@ -1145,26 +1235,19 @@ theorem inv_is_func_of_injective {f A B : ZFSet} {f_is_func : A.IsFunc B f}
       and_intros
       · exact hb
       · use a
-        and_intros
-        · zdom
-        · exact pair_f
     · exact ha
   · intro y hy
     rw [mem_sep] at hy
     obtain ⟨hy, x, hx, pair_f⟩ := hy
     use x
-    have x_A : x ∈ A := by
-      rw [mem_sep] at hx
-      obtain ⟨xA, _, _, _⟩ := hx
-      exact xA
     and_intros <;> beta_reduce
     · unfold inv
       rw [mem_sep, pair_mem_prod, π₁_pair, π₂_pair]
-      exact ⟨⟨hy, x_A⟩, pair_f⟩
+      exact ⟨⟨hy, hx⟩, pair_f⟩
     · intro z hz
       rw [inv, mem_sep, π₁_pair, π₂_pair, pair_mem_prod] at hz
       symm
-      exact hf x z y x_A hz.1.2 hy pair_f hz.2
+      exact hf x z y hx hz.1.2 hy pair_f hz.2
 
 -- macro_rules | `(tactic| zfun) => `(tactic| apply inv_is_func_of_injective; zfun)
 
@@ -1757,18 +1840,17 @@ theorem IsPFunc.empty_dom {f A B : ZFSet} (hf : IsPFunc f A B) (dom_emp : f.Dom
   constructor
   · intro hz
     obtain ⟨x, xA, y, yB, rfl⟩ := mem_prod.mp <| hf.1 hz
-    nomatch notMem_empty _ <| dom_emp ▸ mem_dom hf hz
+    nomatch notMem_empty _ <| dom_emp ▸ mem_dom_of (is_rel_of_is_pfunc hf) hz
   · intro hz
     nomatch notMem_empty _ <| hz
 
 theorem IsPFunc.empty_range_of_empty_dom {f A B : ZFSet}
   (hf : IsPFunc f A B) (dom_emp : f.Dom = ∅) : f.Range = ∅ := by
     unfold Range
-    conv =>
-      arg 1
-      rw [dom_emp, empty_dom hf dom_emp]
-    simp only [notMem_empty, and_self, exists_const, sep_empty_iff,
-      not_false_eq_true, implies_true, or_true]
+    apply empty_dom hf at dom_emp
+    conv => arg 1 ; rw [dom_emp]
+    simp only [notMem_empty, and_false, exists_const, sep_empty_iff, not_false_eq_true,
+      implies_true, or_true]
 
 theorem IsPFunc.exists_dom_of_mem_range {f A B : ZFSet}
   (hf : IsPFunc f A B) {y : ZFSet} (hy : y ∈ f.Range) :
@@ -1777,11 +1859,6 @@ theorem IsPFunc.exists_dom_of_mem_range {f A B : ZFSet}
   rw [mem_sep] at hy
   obtain ⟨y_B, x, x_dom, pair⟩ := hy
   exists x
-  and_intros
-  · unfold Dom at x_dom
-    rw [mem_sep] at x_dom
-    exact x_dom.1
-  · exact pair
 
 theorem IsFunc.surj_on_range {f A B : ZFSet} (hf : IsFunc A B f) :
     IsSurjective (f := f) (A := A) (B := f.Range) (is_func_on_range hf) := by
@@ -1811,9 +1888,6 @@ theorem IsFunc.range_eq_of_surjective {f A B : ZFSet} (hf : IsFunc A B f)
     · exact hy
     · obtain ⟨x, x_dom, xy⟩ := surj y hy
       exists x
-      and_intros
-      · exact ZFSet.mem_dom (is_func_is_pfunc hf) xy
-      · exact xy
 
 -- `ZFSet.instPartialOrder` induces a subset-based order on `{x // x ∈ n}`, which would clash
 -- with the numeric order below. Since Mathlib derives `⊆` on `ZFSet` from that instance, the
@@ -2251,7 +2325,7 @@ def ZFFinSet.inductionOn {P : ZFFinSet → Prop}
           rcases bS with rfl | bS
           · unfold Range at n_range
             simp_rw [mem_sep, mem_insert_iff, true_or, true_and, not_exists, not_and] at n_range
-            nomatch n_range a ⟨aS, b, Or.inl rfl, hz⟩ hz
+            nomatch n_range a aS hz
           · exact bS
         · exact fS_fun.2
       apply IH S fS (mem_funs.mpr this) S_fin this
@@ -2615,7 +2689,7 @@ theorem Min_mem_of_non_empty_finite {S : ZFSet} [inst : LinearOrder {x // x ∈
       exfalso
       obtain ⟨x, hx⟩ := (nonempty_def _).mp S_nemp
       obtain ⟨y, hy, -⟩ := hf.2 x hx
-      have := IsPFunc.mem_range_of_mem (is_func_is_pfunc (mem_funs.mp ‹f ∈ _›)) hy
+      have := mem_range_of (is_rel_of_is_func (mem_funs.mp ‹f ∈ _›)) hy
       rw [IsFunc.range_eq_of_surjective (mem_funs.mp ‹f ∈ _›) bij.2] at this
       nomatch notMem_empty _ this
     | succ n _ => exact ZFNat.succ_ne_zero n
@@ -2630,18 +2704,15 @@ theorem Min_mem_of_non_empty_finite {S : ZFSet} [inst : LinearOrder {x // x ∈
     | succ => exact ZFNat.zero_lt_succ
   rw [mem_sep] at this
   obtain ⟨x₀, x₀_dom, x₀_def⟩ := this.2
-  have x₀_S : x₀ ∈ S := by
-    rw [mem_sep] at x₀_dom
-    exact x₀_dom.1
   by_contra! contr
-  specialize contr x₀ x₀_S
+  specialize contr x₀ x₀_dom
   obtain ⟨_, x₁, x₁_S, x₁_lt_x₀⟩ := contr
   obtain ⟨y₁, y₁_def, -⟩ := hf.2 x₁ x₁_S
-  have := IsPFunc.mem_range_of_mem (is_func_is_pfunc hf) y₁_def
+  have := mem_range_of (is_rel_of_is_func hf) y₁_def
   rw [IsFunc.range_eq_of_surjective hf bij.2] at this
   unfold IsStrictMono at mono
   have : (⟨y₁, ZFNat.mem_Nat_of_mem_mem_Nat hn this⟩ : ZFNat) < 0 := by
-    specialize mono x₁ x₀ y₁ (0:ZFNat) x₁_S this y₁_def x₀_S _ x₀_def _
+    specialize mono x₁ x₀ y₁ (0:ZFNat) x₁_S this y₁_def x₀_dom _ x₀_def _
     · suffices 0 < (⟨n, hn⟩ : ZFNat) from this
       cases h : (⟨n, hn⟩:ZFNat) using ZFNat.cases with
       | zero =>
diff --git a/ZFLean/Integers.lean b/ZFLean/Integers.lean
index 2fccd8f..af476d9 100644
--- a/ZFLean/Integers.lean
+++ b/ZFLean/Integers.lean
@@ -1065,75 +1065,6 @@ lemma Int.nonempty : ZFSet.Int ≠ ∅ := by
   simp only [notMem_empty, iff_false] at h
   nomatch h (ZFSet.ofInt 0) (ZFSet.mem_ofInt_Int 0)
 
-def π₁ (x : ZFSet) : ZFSet := ⋃₀ (⋂₀ x)
-
-open Classical in -- couldn't find another way
-noncomputable def π₂ (x : ZFSet) : ZFSet :=
-  let δ : ZFSet := (⋃₀ x \ ⋂₀ x)
-  if δ = ∅ then π₁ x else ⋃₀ δ
-
-@[simp] theorem π₁_pair (x y : ZFSet) : π₁ (x.pair y) = x := by
-  unfold π₁ pair
-  ext
-  rw [sInter_pair, mem_sUnion]
-  constructor
-  · rintro ⟨w, l, r⟩
-    rw [mem_inter, mem_singleton, mem_pair] at l
-    rw [l.1] at r
-    assumption
-  · intro h
-    exists x
-    rw [mem_inter, mem_singleton, mem_pair]
-    exact ⟨⟨rfl, .inl rfl⟩, h⟩
-
-@[simp] theorem pair_inter {x y : ZFSet} : {x} ∩ {x, y} = ({x} : ZFSet) := by
-    ext
-    rw [mem_inter, mem_singleton, mem_pair]
-    constructor
-    · rintro ⟨rfl, _ | rfl⟩ <;> rfl
-    · rintro rfl
-      exact ⟨rfl, .inl rfl⟩
-
-@[simp] theorem pair_union {x y : ZFSet} : {x} ∪ {x, y} = ({x, y} : ZFSet) := by
-    ext
-    rw [mem_union, mem_singleton, mem_pair]
-    exact or_self_left
-
-@[simp] theorem pair_minus {x y : ZFSet} : x ≠ y → {x, y} \ {x} = ({y} : ZFSet) := by
-  intro x_ne_y
-  ext z
-  rw [mem_sdiff, mem_pair, mem_singleton, mem_singleton]
-  constructor
-  · rintro ⟨rfl | rfl, r⟩
-    · contradiction
-    · rfl
-  · rintro rfl
-    exact ⟨.inr rfl, x_ne_y ∘ Eq.symm⟩
-
-@[simp] theorem π₂_pair (x y : ZFSet) : π₂ (x.pair y) = y := by
-  unfold π₂
-  dsimp
-  split_ifs with h
-  · rw [π₁_pair]
-    unfold pair at h
-    rw [sUnion_pair, pair_union, sInter_pair, pair_inter] at h
-    rw [ZFSet.ext_iff] at h
-    specialize h y
-    simpa only [mem_sdiff, mem_insert_iff, mem_singleton, eq_self,
-      or_true, true_and, notMem_empty, iff_false, not_not, eq_comm] using h
-  · unfold pair at *
-    rw [sUnion_pair, pair_union, sInter_pair, pair_inter] at h ⊢
-    rw [pair_minus]
-    · exact sUnion_singleton
-    · intro h'
-      rw [h'] at h
-      simp [ZFSet.ext_iff] at h
-
-theorem pair_eta {z A B : ZFSet} (h : z ∈ A.prod B) : z = z.π₁.pair z.π₂ := by
-  rw [mem_prod] at h
-  obtain ⟨a, ha, b, hb, rfl⟩ := h
-  rw [π₁_pair, π₂_pair]
-
 theorem mem_Int_proj {x : ZFSet} (h : x ∈ Int) :
   ∃ n ∈ Nat, (x.π₁ = ∅ ∧ x.π₂ = n) ∨ (x.π₁ = n ∧ x.π₂ = ∅) := by
   simp_rw [mem_union, mem_prod] at h
diff --git a/ZFLean/Quotient.lean b/ZFLean/Quotient.lean
new file mode 100644
index 0000000..3c2791e
--- /dev/null
+++ b/ZFLean/Quotient.lean
@@ -0,0 +1,299 @@
+module
+
+public import Mathlib.SetTheory.ZFC.Basic
+public import ZFLean.Def
+import ZFLean.Tactics
+public import ZFLean.Functions
+
+public section
+
+namespace ZFSet
+
+open Classical in
+def equivZFRelation (E : ZFSet) : Equiv { R : ZFSet // R ⊆ E.prod E } (E → E → Prop) where
+  toFun R := fun x y => x.val.pair y.val ∈ R.val
+  invFun r := ⟨E.prod E |>.sep  fun p => if h : p ∈ E.prod E then
+      r
+      ⟨p.π₁, by
+        rw [mem_prod] at h
+        obtain ⟨x, hx, y, hy, rfl⟩ := h
+        rw [π₁_pair]
+        exact hx
+      ⟩
+      ⟨p.π₂, by
+        rw [mem_prod] at h
+        obtain ⟨x, hx, y, hy, rfl⟩ := h
+        rw [π₂_pair]
+        exact hy
+      ⟩
+    else False,
+    sep_subset⟩
+  left_inv R := by
+    ext p
+    dsimp only
+    rw [mem_sep, ←exists_prop]
+    conv => enter [1, 1, h] ; rw [dif_pos h]
+    rw [mem_prod, exists_prop, ←exists_and_right]
+    conv =>
+      enter [1, 1, x]
+      rw [and_assoc, ←exists_and_right]
+      conv =>
+        enter [2, 1, y]
+        rw [and_assoc]
+        conv =>
+          right
+          rw [←exists_prop]
+          conv => enter [1, h] ; rw [h, π₁_pair, π₂_pair, ←h]
+          rw [exists_prop]
+        rw [←and_assoc]
+      rw [exists_and_right, ←and_assoc]
+    rw [exists_and_right, ←mem_prod, and_iff_right_of_imp (R.prop ·)]
+  right_inv r := by
+    ext ⟨x, hx⟩ ⟨y, hy⟩
+    dsimp only
+    rw [mem_sep, ←exists_prop]
+    conv =>
+      enter [1, 1, h]
+      rw [dif_pos h]
+      conv =>
+        congr <;> left
+        · rw [π₁_pair]
+        · rw [π₂_pair]
+      change r ⟨x, hx⟩ ⟨y, hy⟩
+    rw [exists_prop, pair_mem_prod, and_iff_right ⟨hx, hy⟩]
+
+instance (E : ZFSet) : TransferEquiv { R : ZFSet // R ⊆ E.prod E } (E → E → Prop) where
+  equiv := E.equivZFRelation
+
+theorem equivZFRelation_related (E : ZFSet) (R : { R : ZFSet // R ⊆ E.prod E }) (x y : E) :
+    E.equivZFRelation R x y = (x.val.pair y.val ∈ R.val) := by
+  unfold equivZFRelation
+  dsimp
+
+theorem equivZFRelation_Reflexivity (E : ZFSet) (R : { R : ZFSet // R ⊆ E.prod E }) :
+    (∀ x, E.equivZFRelation R x x) = is_rel_reflexive R.val R.prop := by
+  conv =>
+    rw [is_rel_reflexive_iff]
+    left
+    conv => ext x ; rw [equivZFRelation_related]
+    rw [Subtype.forall]
+
+theorem equivZFRelation_Symmetry (E : ZFSet) (R : { R : ZFSet // R ⊆ E.prod E }) :
+    (∀ x y, E.equivZFRelation R x y → E.equivZFRelation R y x) = is_rel_symmetric R.val R.prop := by
+  conv =>
+    rw [is_rel_symmetric_iff _ R.prop]
+    left
+    conv => enter [x, y] ; rw [equivZFRelation_related, equivZFRelation_related]
+    repeat rw [Subtype.forall] ; ext v ; (conv => repeat rw [forall_comm] ; ext _)
+    dsimp only
+    rw [←and_imp, ←pair_mem_prod, ←and_imp, and_iff_right_of_imp (R.prop ·)]
+  ext
+  constructor
+  · intro h x y
+    exact ⟨(h x y ·), (h y x ·)⟩
+  · intro h x y
+    exact Iff.mp <| h x y
+
+theorem equivZFRelation_Transitivity (E : ZFSet) (R : { R : ZFSet // R ⊆ E.prod E }) :
+    (∀ x y z, E.equivZFRelation R x y → E.equivZFRelation R y z → E.equivZFRelation R x z)
+      = is_rel_transitive R.val R.prop := by
+  conv =>
+    rw [is_rel_transitive_iff _ R.prop]
+    left
+    conv =>
+      enter [_, _, _]
+      rw [equivZFRelation_related, equivZFRelation_related, equivZFRelation_related]
+    repeat
+      rw [Subtype.forall]
+      ext x
+      conv => repeat
+        rw [forall_comm]
+        ext h
+        conv => pattern (occs := *) _ → _ → _
+    dsimp only
+    rw [←and_imp, ←and_imp, and_assoc, ←and_imp, ←and_imp, and_assoc]
+    left
+    conv =>
+      left
+      conv => enter [2, 1] ; rw [←and_self (_ ∈ E)]
+      rw [and_assoc, ←pair_mem_prod, ←and_assoc, ←pair_mem_prod]
+    rw [and_iff_right_of_imp fun ⟨l,r⟩ => ⟨R.prop l, R.prop r⟩]
+
+theorem equivZFRelation_Equivalence (E : ZFSet) (R : { R : ZFSet // R ⊆ E.prod E }) :
+    Equivalence (E.equivZFRelation R) = is_rel_equivalence R.val R.prop := by
+  ext
+  rw [is_rel_equivalence, ←equivZFRelation_Reflexivity, ←equivZFRelation_Symmetry,
+    ←equivZFRelation_Transitivity]
+  constructor <;> intro ⟨r, s, t⟩ <;> [split_ands ; constructor] <;> assumption
+
+theorem ZFEquiv_of_Equivalence (E : ZFSet) (r : E → E → Prop) (re : Equivalence r) :
+    (E.equivZFRelation.symm r).val.is_rel_equivalence (E.equivZFRelation.symm r).prop :=
+  (equivZFRelation_Equivalence E (E.equivZFRelation.symm r)).mp
+    ( by rw [@Equiv.apply_symm_apply] ; exact re)
+
+@[expose]
+def ZFQuotient (E R : ZFSet) : ZFSet :=
+  E.powerset.sep (fun c => ∃ x ∈ c, ∀ y : ZFSet, y ∈ c ↔ x.pair y ∈ R)
+
+namespace ZFQuotient
+
+variable
+  {E R : ZFSet}
+
+
+def class_of (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) (x : E) :
+    E.ZFQuotient R :=
+  ⟨E.sep fun y => x.val.pair y ∈ R, by
+    rw [ZFQuotient, mem_sep, mem_powerset]
+    exists sep_subset, x
+    rw [mem_sep]
+    rw [is_rel_equivalence, R.is_rel_reflexive_iff hrR, R.is_rel_symmetric_iff hrR] at heR
+    exists ⟨x.prop, heR.left x x.prop⟩
+    intro y
+    rw [mem_sep, and_iff_right_of_imp (And.right <| pair_mem_prod.mp <| hrR ·)]
+  ⟩
+
+theorem mem_class_of_self (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) (x : E) :
+    x.val ∈ (class_of hrR heR x).val := by
+  rw [class_of, mem_sep]
+  constructor
+  · exact x.prop
+  · rw [is_rel_equivalence, R.is_rel_reflexive_iff] at heR
+    exact heR.left x x.prop
+
+theorem mem_class_of_iff_related (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) (x : E) (y : ZFSet) :
+    y ∈ (class_of hrR heR x).val ↔ y.pair x.val ∈ R := by
+  rw [class_of, mem_sep, and_iff_right_of_imp (And.right <| pair_mem_prod.mp <| hrR ·)]
+  rw [is_rel_equivalence, R.is_rel_symmetric_iff hrR] at heR
+  exact heR.right.left x y
+
+
+def of_in_class {C : E.ZFQuotient R} (w : C.val) : E :=
+  ⟨w |>.val, (mem_powerset.mp <| And.left <| mem_sep.mp C.prop) w.prop⟩
+
+theorem class_of_mem_eq_self (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) (C : E.ZFQuotient R) (x : C.val) :
+    class_of hrR heR (of_in_class x) = C := by
+  obtain ⟨x, hx⟩ := x
+  obtain ⟨C, hC⟩ := C
+  obtain ⟨hC', ⟨z,hz,extC⟩⟩ := mem_sep.mp hC
+  rw [of_in_class, class_of]
+  ext y
+  dsimp only
+  rw [mem_sep, and_iff_right_of_imp (And.right <| pair_mem_prod.mp <| hrR ·)]
+  rw [extC]
+  rw [is_rel_equivalence, R.is_rel_transitive_iff, R.is_rel_symmetric_iff] at heR
+  let ⟨r, s, t⟩ := heR
+  constructor
+  · intro xy_related
+    exact t z x y ⟨(extC x |>.mp hx), xy_related⟩
+  · intro zy_related
+    exact t x z y ⟨s z x |>.mp (extC x |>.mp hx), zy_related⟩
+
+theorem class_eq_iff_related (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) (x y : E) :
+    class_of hrR heR x = class_of hrR heR y ↔ x.val.pair y.val ∈ R := by
+  constructor
+  · intro h
+    rw [←mem_class_of_iff_related hrR heR, ←h]
+    exact mem_class_of_self hrR heR x
+  · intro xy_related
+    obtain ⟨x, x_E⟩ := x
+    rw [←mem_class_of_iff_related hrR heR] at xy_related
+    change class_of _ _ (of_in_class ⟨x, xy_related⟩) = _
+    rw [class_of_mem_eq_self hrR heR]
+
+@[expose]
+noncomputable def choose_repr (C : E.ZFQuotient R) : C.val :=
+    let hC := mem_sep.mp C.prop
+    ⟨hC.right.choose, hC.right.choose_spec.left⟩
+
+noncomputable def lift
+    (f : E → α) (C : E.ZFQuotient R) : α :=
+  (f (of_in_class (choose_repr C)))
+
+theorem lift_class_of (hrR : R ⊆ E.prod E := by zrel)
+(heR : R.is_rel_equivalence hrR := by assumption) (f : E → α)
+(h : ∀ a b, a.val.pair b.val ∈ R → f a = f b) (x : E) :
+    lift f (class_of hrR heR x) = f x := by
+  apply h
+  rw [of_in_class, ←mem_class_of_iff_related hrR heR]
+  exact Subtype.prop <| choose_repr <| class_of _ _ x
+
+@[expose]
+def toSetoid {E R : ZFSet}
+    (hrR : R ⊆ E.prod E := by zrel)
+    (heR : R.is_rel_equivalence hrR := by assumption) : Setoid E where
+  r :=  E.equivZFRelation ⟨R, hrR⟩
+  iseqv := E.equivZFRelation_Equivalence ⟨R, hrR⟩ |>.mpr heR
+
+
+
+noncomputable def equivZFQuotient (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) :
+    Equiv (ZFQuotient E R) (Quotient <| toSetoid  hrR heR) where
+  toFun C := lift (fun x => ⟦x⟧) C
+  invFun W := Quotient.liftOn W (fun W => class_of hrR heR W) (by
+    intro a b related
+    change a.val.pair b.val ∈ R at related
+    exact (class_eq_iff_related hrR heR a b).mpr related
+    )
+  left_inv := by
+    intro C
+    dsimp only
+    let W := choose_repr C
+    rw [←class_of_mem_eq_self hrR heR C, lift_class_of _ _ _ _ (of_in_class W),Quotient.liftOn_mk]
+    intro a b related
+    rw [Quotient.eq]
+    exact related
+  right_inv := by
+    intro W
+    cases W using Quotient.ind
+    rename_i W
+    dsimp only
+    generalize_proofs h
+    rw [Quotient.liftOn_mk, lift_class_of _ _ _]
+    intro a b related
+    rw [Quotient.eq]
+    exact related
+
+noncomputable def equivZFQuotient_of_rel {r : E → E → Prop} (re : Equivalence r) :
+    Equiv (E.ZFQuotient <| E.equivZFRelation.symm r) (Quotient ⟨r,re⟩) :=
+  Equiv.trans
+    (
+      equivZFQuotient _
+        <| (equivZFRelation_Equivalence E (E.equivZFRelation.symm r)).mp
+          ( by rw [@Equiv.apply_symm_apply] ; exact re)
+    )
+    ( by
+      apply Quotient.congrRight
+      unfold toSetoid
+      dsimp only
+      rw [Subtype.eta, E.equivZFRelation.apply_symm_apply]
+      intro _ _
+      rfl
+    )
+
+@[expose]
+noncomputable def equivZFProdProd {E F : ZFSet} : Equiv (E.prod F) (E × F) where
+  toFun p := (
+    ⟨p.val.π₁, by obtain ⟨_,_,_,_,hp⟩ := mem_prod.mp p.prop ; rwa [hp, π₁_pair]⟩,
+    ⟨p.val.π₂, by obtain ⟨_,_,_,_,hp⟩ := mem_prod.mp p.prop ; rwa [hp, π₂_pair]⟩
+  )
+  invFun p := ⟨p.1.val.pair p.2.val, pair_mem_prod.mpr <| ⟨p.1.prop, p.2.prop⟩⟩
+  left_inv p := by
+    obtain ⟨x,hx,y,hy,hp⟩ := mem_prod.mp p.prop
+    simp_rw [Subtype.ext_iff, hp, π₁_pair, π₂_pair]
+  right_inv p := by
+    dsimp only
+    simp_rw [Prod.ext_iff,Subtype.ext_iff, π₁_pair, π₂_pair]
+    trivial
+
+end ZFQuotient
+
+end ZFSet
+
+end
diff --git a/ZFLean/Rationals.lean b/ZFLean/Rationals.lean
index 4c11ded..524dbe8 100644
--- a/ZFLean/Rationals.lean
+++ b/ZFLean/Rationals.lean
@@ -7,6 +7,7 @@ module
 
 public import ZFLean.Integers
 import ZFLean.TransferAlgebra
+public import ZFLean.Quotient
 import Mathlib.Data.Rat.Cast.Order
 import Mathlib.Tactic.Ring
 
@@ -887,6 +888,118 @@ attribute [transfer_simps ←] equivRat_le equivRat_lt
 end Transfer
 
 end ZFRat
+
+/- The carrier set of Rat, which is equivalent to the carrier type of ZFRat -/
+noncomputable def zf_qcarrier := Int.prod (Int \ {(0 : ZFInt).into.val} )
+noncomputable def zf_qcarrier_equiv_qcarrier :
+  zf_qcarrier ≃ ZFInt × ZFInt'  :=
+  Equiv.trans (@ZFQuotient.equivZFProdProd Int (Int \ {(0 : ZFInt).into.val} )) <|
+  Equiv.prodCongr ({
+    toFun := ZFInt.outof
+    invFun := ZFInt.into
+    left_inv := ZFInt.into_outof
+    right_inv := ZFInt.outof_into
+  }) ({
+    toFun := fun ⟨z, hz⟩ => ⟨ZFInt.outof ⟨z, sdiff_subset hz⟩, by
+      have hz' := hz
+      rw [mem_sdiff, mem_singleton] at hz
+      obtain not_zero := hz.right
+      intro this
+      apply congr_arg ZFInt.into at this
+      rw [ZFInt.into_outof, Subtype.ext_iff] at this
+      exact not_zero this
+    ⟩
+    invFun := fun ⟨z, nz ⟩ => ⟨ZFInt.into z, by
+      rw [mem_sdiff, mem_singleton]
+      exists (ZFInt.into z).prop
+      intro h
+      rw [←Subtype.ext_iff] at h
+      apply ZFInt.into_inj at h
+      exact nz h
+    ⟩
+    left_inv := by
+      intro ⟨z, hz⟩
+      dsimp only
+      rw [Subtype.ext_iff]
+      change ZFInt.into _ = z
+      rw [ZFInt.into_outof]
+    right_inv := by
+      intro ⟨z, nz⟩
+      rw [Subtype.ext_iff]
+      dsimp only
+      apply ZFInt.into_inj
+      rw [ZFInt.into_outof, Subtype.ext_iff]
+  })
+
+/- The relation equivalence of Rat, which is equivalent to equivalence relation of ZFRat -/
+open Classical in
+@[expose]
+noncomputable def zf_qrel : ZFSet := (zf_qcarrier.prod zf_qcarrier).sep fun pq =>
+  if h : pq ∈ zf_qcarrier.prod zf_qcarrier then
+    let h := mem_prod.mp h
+    let pn : ZFInt := ZFInt.outof ⟨pq.π₁.π₁, by
+      obtain ⟨p,hp, _,_, rfl⟩ := h
+      rw [zf_qcarrier, mem_prod] at hp
+      obtain ⟨pn, hpn, pd, hpd, rfl⟩ := hp
+      rwa [π₁_pair,π₁_pair]
+    ⟩
+    let pd : ZFInt := ZFInt.outof ⟨pq.π₁.π₂, by
+      obtain ⟨p,hp, _,_, rfl⟩ := h
+      rw [zf_qcarrier, mem_prod] at hp
+      obtain ⟨pn, hpn, pd, hpd, rfl⟩ := hp
+      rw [π₁_pair,π₂_pair]
+      exact sdiff_subset hpd
+    ⟩
+    let qn : ZFInt := ZFInt.outof ⟨pq.π₂.π₁, by
+      obtain ⟨p,hp, q, hq, rfl⟩ := h
+      rw [zf_qcarrier, mem_prod] at hq
+      obtain ⟨pn, hpn, pd, hpd, rfl⟩ := hq
+      rwa [π₂_pair,π₁_pair]
+    ⟩
+    let qd : ZFInt := ZFInt.outof ⟨pq.π₂.π₂, by
+      obtain ⟨p,hp, q, hq, rfl⟩ := h
+      rw [zf_qcarrier, mem_prod] at hq
+      obtain ⟨pn, hpn, pd, hpd, rfl⟩ := hq
+      rw [π₂_pair,π₂_pair]
+      exact sdiff_subset hpd
+    ⟩
+    pn * qd = pd * qn
+  else False
+
+open Classical in
+theorem zf_qrel_equiv_qrel :
+    zf_qcarrier.equivZFRelation ⟨zf_qrel, sep_subset⟩ =
+    (Function.onFun ZFSet.qrel zf_qcarrier_equiv_qcarrier) := by
+  ext x y
+  rw [equivZFRelation_related, Function.onFun, ZFSet.qrel]
+  dsimp only
+  rw [zf_qrel, mem_sep]
+  conv =>
+    enter [1, 1]
+    discharge => rw [pair_mem_prod] ; exact ⟨x.prop, y.prop⟩
+  rw [true_and, dif_pos <| pair_mem_prod.mpr ⟨x.prop, y.prop⟩]
+  dsimp only
+  rw [←propext_iff]
+  congr <;> simp only [π₁_pair, π₂_pair]
+
+theorem zf_qrel_eq : zf_qrel.is_rel_equivalence sep_subset :=  by
+  apply zf_qcarrier.equivZFRelation_Equivalence ⟨zf_qrel, sep_subset⟩ |>.mp
+  rw [zf_qrel_equiv_qrel]
+  exact Equivalence.comap ZFSet.qrel_eq zf_qcarrier_equiv_qcarrier.toFun
+
+/- The set of Rational numbers -/
+noncomputable def Rat : ZFSet := Int.prod (Int \ {(0 : ZFInt).into.val} ) |>.ZFQuotient zf_qrel
+
+noncomputable def equivRatZFRat : Rat ≃ ZFRat :=
+  Equiv.trans
+  (@ZFQuotient.equivZFQuotient zf_qcarrier zf_qrel sep_subset zf_qrel_eq)
+  (Quotient.congr zf_qcarrier_equiv_qcarrier (by
+    unfold ZFSet.instSetoidZFIntZFInt' ZFQuotient.toSetoid
+    dsimp only
+    intro x y
+    rw [zf_qrel_equiv_qrel]
+  ))
+
 end Rationals
 end ZFSet