P. 88 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8701-8800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ertr3d 8701	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐵𝑅𝐴)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	ertr4d 8702	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	erref 8703	An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐴)
Theorem	ercnv 8704	The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅)
Theorem	errn 8705	The range and domain of an equivalence relation are equal. (Contributed by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → ran 𝑅 = 𝐴)
Theorem	erssxp 8706	An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴))
Theorem	erex 8707	An equivalence relation is a set if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → (𝐴 ∈ 𝑉 → 𝑅 ∈ V))
Theorem	erexb 8708	An equivalence relation is a set if and only if its domain is a set. (Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → (𝑅 ∈ V ↔ 𝐴 ∈ V))
Theorem	iserd 8709*	A reflexive, symmetric, transitive relation is an equivalence relation on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → Rel 𝑅)    &   ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦𝑅𝑥)    &   ⊢ ((𝜑 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥))    ⇒   ⊢ (𝜑 → 𝑅 Er 𝐴)
Theorem	iseri 8710*	A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 8709, which avoids the need to provide a "dummy antecedent" 𝜑 if there is no natural one to choose. (Contributed by AV, 30-Apr-2021.)
⊢ Rel 𝑅    &   ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥)    &   ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)    &   ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)    ⇒   ⊢ 𝑅 Er 𝐴
Theorem	iseriALT 8711*	Alternate proof of iseri 8710, avoiding the usage of mptru 1570 and ⊤ as antecedent by using ax-mp 5 and one of the hypotheses as antecedent. This results, however, in a slightly longer proof. (Contributed by AV, 30-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Rel 𝑅    &   ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥)    &   ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)    &   ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)    ⇒   ⊢ 𝑅 Er 𝐴
Theorem	brinxper 8712*	Conditions for a reflexive, symmetric and transitive binary relation to be an equivalence relation over a class 𝑉. (Contributed by AV, 11-Jun-2025.)
⊢ (𝑥 ∈ 𝑉 → 𝑥 ∼ 𝑥)    &   ⊢ (𝑥 ∈ 𝑉 → (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥))    &   ⊢ (𝑥 ∈ 𝑉 → ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧))    ⇒   ⊢ ( ∼ ∩ (𝑉 × 𝑉)) Er 𝑉
Theorem	brdifun 8713	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	swoer 8714*	Incomparability under a strict weak partial order is an equivalence relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    ⇒   ⊢ (𝜑 → 𝑅 Er 𝑋)
Theorem	swoord1 8715*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
Theorem	swoord2 8716*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵))
Theorem	swoso 8717*	If the incomparability relation is equivalent to equality in a subset, then the partial order strictly orders the subset. (Contributed by Mario Carneiro, 30-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝑌 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ∧ 𝑥𝑅𝑦)) → 𝑥 = 𝑦)    ⇒   ⊢ (𝜑 → < Or 𝑌)
Theorem	eqerlem 8718*	Lemma for eqer 8719. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)
Theorem	eqer 8719*	Equivalence relation involving equality of dependent classes 𝐴(𝑥) and 𝐵(𝑦). (Contributed by NM, 17-Mar-2008.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof shortened by AV, 1-May-2021.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ 𝑅 Er V
Theorem	ider 8720	The identity relation is an equivalence relation. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 9-Jul-2014.)
⊢ I Er V
Theorem	0er 8721	The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 1-May-2021.)
⊢ ∅ Er ∅
Theorem	eceq1 8722	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq1d 8723	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq2 8724	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵)
Theorem	eceq2i 8725	Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ [𝐶]𝐴 = [𝐶]𝐵
Theorem	eceq2d 8726	Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵)
Theorem	elecg 8727	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	ecref 8728	All elements are in their own equivalence class. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ ((𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴]𝑅)
Theorem	elec 8729	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)
Theorem	relelec 8730	Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	elecres 8731	Elementhood in the restricted coset of 𝐵. (Contributed by Peter Mazsa, 21-Sep-2018.)
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ [𝐵](𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))
Theorem	elecreseq 8732	The restricted coset of 𝐵 when 𝐵 is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018.)
⊢ (𝐵 ∈ 𝐴 → [𝐵](𝑅 ↾ 𝐴) = [𝐵]𝑅)
Theorem	elecex 8733	Condition for a coset to be a set. (Contributed by Peter Mazsa, 4-May-2019.)
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ V))
Theorem	ecss 8734	An equivalence class is a subset of the domain. (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    ⇒   ⊢ (𝜑 → [𝐴]𝑅 ⊆ 𝑋)
Theorem	ecdmn0 8735	A representative of a nonempty equivalence class belongs to the domain of the equivalence relation. (Contributed by NM, 15-Feb-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ dom 𝑅 ↔ [𝐴]𝑅 ≠ ∅)
Theorem	ereldm 8736	Equality of equivalence classes implies equivalence of domain membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅)    ⇒   ⊢ (𝜑 → (𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋))
Theorem	erth 8737	Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Theorem	erth2 8738	Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership of the second argument in the domain. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Theorem	erthi 8739	Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅)
Theorem	erdisj 8740	Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83. (Contributed by NM, 15-Jun-2004.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝑅 Er 𝑋 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅))
Theorem	ecidsn 8741	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
⊢ [𝐴] I = {𝐴}
Theorem	qseq1 8742	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶))
Theorem	qseq2 8743	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵))
Theorem	qseq2i 8744	Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 / 𝐴) = (𝐶 / 𝐵)
Theorem	qseq1d 8745	Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶))
Theorem	qseq2d 8746	Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 / 𝐴) = (𝐶 / 𝐵))
Theorem	qseq12 8747	Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 / 𝐶) = (𝐵 / 𝐷))
Theorem	0qs 8748	Quotient set with the empty set. (Contributed by Peter Mazsa, 14-Sep-2019.)
⊢ (∅ / 𝑅) = ∅
Theorem	elqsg 8749*	Closed form of elqs 8750. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅))
Theorem	elqs 8750*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsi 8751*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsecl 8752*	Membership in a quotient set by an equivalence class according to ∼. (Contributed by Alexander van der Vekens, 12-Apr-2018.) (Revised by AV, 30-Apr-2021.)
⊢ (𝐵 ∈ 𝑋 → (𝐵 ∈ (𝑊 / ∼ ) ↔ ∃𝑥 ∈ 𝑊 𝐵 = {𝑦 ∣ 𝑥 ∼ 𝑦}))
Theorem	ecelqs 8753	Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ (((𝑅 ↾ 𝐴) ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
Theorem	ecelqsw 8754	Membership of an equivalence class in a quotient set. More restrictive antecedent; kept for backward compatibility; for new work, prefer ecelqs 8753. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) (Proof shortened by AV, 25-Nov-2025.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
Theorem	ecelqsi 8755	Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑅 ∈ V    ⇒   ⊢ (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
Theorem	ecopqsi 8756	"Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.)
⊢ 𝑅 ∈ V    &   ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅)    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [⟨𝐵, 𝐶⟩]𝑅 ∈ 𝑆)
Theorem	qsexg 8757	A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V)
Theorem	qsex 8758	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 / 𝑅) ∈ V
Theorem	uniqs 8759	The union of a quotient set, like uniqsw 8760 but with a weaker antecedent: only the restriction of 𝑅 by 𝐴 needs to be a set, not 𝑅 itself, see e.g. cnvepima 38843. (Contributed by NM, 9-Dec-2008.) (Revised by Peter Mazsa, 20-Jun-2019.)
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴))
Theorem	uniqsw 8760	The union of a quotient set. More restrictive antecedent; kept for backward compatibility; for new work, prefer uniqs 8759. (Contributed by NM, 9-Dec-2008.) (Proof shortened by AV, 25-Nov-2025.)
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴))
Theorem	qsss 8761	A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝐴)    ⇒   ⊢ (𝜑 → (𝐴 / 𝑅) ⊆ 𝒫 𝐴)
Theorem	uniqs2 8762	The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴)
Theorem	snecg 8763	The singleton of a coset is the singleton quotient. (Contributed by Peter Mazsa, 25-Mar-2019.)
⊢ (𝐴 ∈ 𝑉 → {[𝐴]𝑅} = ({𝐴} / 𝑅))
Theorem	snec 8764	The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅)
Theorem	ecqs 8765	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
⊢ 𝑅 ∈ V    ⇒   ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅)
Theorem	ecid 8766	A set is equal to its coset under the converse membership relation. (Note: the converse membership relation is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ [𝐴]◡ E = 𝐴
Theorem	qsid 8767	A set is equal to its quotient set modulo the converse membership relation. (Note: the converse membership relation is not an equivalence relation.) (Contributed by NM, 13-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 / ◡ E ) = 𝐴
Theorem	ectocld 8768*	Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑆 = (𝐵 / 𝑅)    &   ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑)    ⇒   ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓)
Theorem	ectocl 8769*	Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑆 = (𝐵 / 𝑅)    &   ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑆 → 𝜓)
Theorem	elqsn0 8770	A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995.)
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅)
Theorem	ecelqsdm 8771	Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.)
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴)
Theorem	ecelqsdmb 8772	𝑅-coset of 𝐵 in a quotient set, biconditional version. (Contributed by Peter Mazsa, 17-Apr-2019.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ (((𝑅 ↾ 𝐴) ∈ 𝑉 ∧ dom 𝑅 = 𝐴) → ([𝐵]𝑅 ∈ (𝐴 / 𝑅) ↔ 𝐵 ∈ 𝐴))
Theorem	eceldmqs 8773	𝑅-coset in its domain quotient. This is the bridge between 𝐴 in the domain and its block [𝐴]𝑅 in its domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.) (Revised by Peter Mazsa, 22-Nov-2025.)
⊢ (𝑅 ∈ 𝑉 → ([𝐴]𝑅 ∈ (dom 𝑅 / 𝑅) ↔ 𝐴 ∈ dom 𝑅))
Theorem	xpider 8774	A Cartesian square is an equivalence relation (in general, it is not a poset). (Contributed by FL, 31-Jul-2009.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝐴 × 𝐴) Er 𝐴
Theorem	iiner 8775*	The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵)
Theorem	riiner 8776*	The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ((𝐵 × 𝐵) ∩ ∩ 𝑥 ∈ 𝐴 𝑅) Er 𝐵)
Theorem	erinxp 8777	A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑅 Er 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (𝑅 ∩ (𝐵 × 𝐵)) Er 𝐵)
Theorem	ecinxp 8778	Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴)))
Theorem	qsinxp 8779	Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴))))
Theorem	qsdisj 8780	Members of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 / 𝑅))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 / 𝑅))    ⇒   ⊢ (𝜑 → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅))
Theorem	qsdisj2 8781*	A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.)
⊢ (𝑅 Er 𝑋 → Disj 𝑥 ∈ (𝐴 / 𝑅)𝑥)
Theorem	qsel 8782	If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ ((𝑅 Er 𝑋 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅)
Theorem	uniinqs 8783	Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4891. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.)
⊢ 𝑅 Er 𝑋    ⇒   ⊢ ((𝐵 ⊆ (𝐴 / 𝑅) ∧ 𝐶 ⊆ (𝐴 / 𝑅)) → ∪ (𝐵 ∩ 𝐶) = (∪ 𝐵 ∩ ∪ 𝐶))
Theorem	qliftlem 8784*	Lemma for theorems about a function lift. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅))
Theorem	qliftrel 8785*	𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌))
Theorem	qliftel 8786*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴)))
Theorem	qliftel1 8787*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴)
Theorem	qliftfun 8788*	The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝐴 = 𝐵)))
Theorem	qliftfund 8789*	The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → Fun 𝐹)
Theorem	qliftfuns 8790*	The function 𝐹 is the unique function defined by 𝐹‘[𝑥] = 𝐴, provided that the well-definedness condition holds. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑦∀𝑧(𝑦𝑅𝑧 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴)))
Theorem	qliftf 8791*	The domain and codomain of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌))
Theorem	qliftval 8792*	The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵)
Theorem	ecoptocl 8793*	Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.)
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅)    &   ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑆 → 𝜓)
Theorem	2ecoptocl 8794*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.)
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅)    &   ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒)
Theorem	3ecoptocl 8795*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.)
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅)    &   ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ([⟨𝑣, 𝑢⟩]𝑅 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃)
Theorem	brecop 8796*	Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.)
⊢ ∼ ∈ V    &   ⊢ ∼ Er (𝐺 × 𝐺)    &   ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ )    &   ⊢ ≤ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ∼ ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ∼ ) ∧ 𝜑))}    &   ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([⟨𝑧, 𝑤⟩] ∼ = [⟨𝐴, 𝐵⟩] ∼ ∧ [⟨𝑣, 𝑢⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) → (𝜑 ↔ 𝜓)))    ⇒   ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ ≤ [⟨𝐶, 𝐷⟩] ∼ ↔ 𝜓))
Theorem	brecop2 8797	Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis. (Contributed by NM, 13-Feb-1996.) (Revised by AV, 12-Jul-2022.)
⊢ dom ∼ = (𝐺 × 𝐺)    &   ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ )    &   ⊢ 𝑅 ⊆ (𝐻 × 𝐻)    &   ⊢ ≤ ⊆ (𝐺 × 𝐺)    &   ⊢ ¬ ∅ ∈ 𝐺    &   ⊢ dom + = (𝐺 × 𝐺)    &   ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶)))    ⇒   ⊢ ([⟨𝐴, 𝐵⟩] ∼ 𝑅[⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) ≤ (𝐵 + 𝐶))
Theorem	eroveu 8798*	Lemma for erov 8800 and eroprf 8801. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐽 = (𝐴 / 𝑅)    &   ⊢ 𝐾 = (𝐵 / 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑅 Er 𝑈)    &   ⊢ (𝜑 → 𝑆 Er 𝑉)    &   ⊢ (𝜑 → 𝑇 Er 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑊)    &   ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Theorem	erovlem 8799*	Lemma for erov 8800 and eroprf 8801. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ 𝐽 = (𝐴 / 𝑅)    &   ⊢ 𝐾 = (𝐵 / 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑅 Er 𝑈)    &   ⊢ (𝜑 → 𝑆 Er 𝑉)    &   ⊢ (𝜑 → 𝑇 Er 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑊)    &   ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)}    ⇒   ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))))
Theorem	erov 8800*	The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ 𝐽 = (𝐴 / 𝑅)    &   ⊢ 𝐾 = (𝐵 / 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑅 Er 𝑈)    &   ⊢ (𝜑 → 𝑆 Er 𝑉)    &   ⊢ (𝜑 → 𝑇 Er 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑊)    &   ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)}    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵) → ([𝑃]𝑅 ⨣ [𝑄]𝑆) = [(𝑃 + 𝑄)]𝑇)