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	brinxper 8701*	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 8702	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	swoer 8703*	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 8704*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
Theorem	swoord2 8705*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵))
Theorem	swoso 8706*	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 8707*	Lemma for eqer 8708. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)
Theorem	eqer 8708*	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 8709	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 8710	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 8711	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq1d 8712	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq2 8713	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵)
Theorem	eceq2i 8714	Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ [𝐶]𝐴 = [𝐶]𝐵
Theorem	eceq2d 8715	Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵)
Theorem	elecg 8716	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	ecref 8717	All elements are in their own equivalence class. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ ((𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴]𝑅)
Theorem	elec 8718	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)
Theorem	relelec 8719	Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	elecres 8720	Elementhood in the restricted coset of 𝐵. (Contributed by Peter Mazsa, 21-Sep-2018.)
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ [𝐵](𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)))
Theorem	elecreseq 8721	The restricted coset of 𝐵 when 𝐵 is an element of the restriction. (Contributed by Peter Mazsa, 16-Oct-2018.)
⊢ (𝐵 ∈ 𝐴 → [𝐵](𝑅 ↾ 𝐴) = [𝐵]𝑅)
Theorem	elecex 8722	Condition for a coset to be a set. (Contributed by Peter Mazsa, 4-May-2019.)
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ V))
Theorem	ecss 8723	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 8724	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 8725	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 8726	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 8727	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 8728	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 8729	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 8730	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
⊢ [𝐴] I = {𝐴}
Theorem	qseq1 8731	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶))
Theorem	qseq2 8732	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵))
Theorem	qseq2i 8733	Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 / 𝐴) = (𝐶 / 𝐵)
Theorem	qseq1d 8734	Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶))
Theorem	qseq2d 8735	Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 / 𝐴) = (𝐶 / 𝐵))
Theorem	qseq12 8736	Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 / 𝐶) = (𝐵 / 𝐷))
Theorem	0qs 8737	Quotient set with the empty set. (Contributed by Peter Mazsa, 14-Sep-2019.)
⊢ (∅ / 𝑅) = ∅
Theorem	elqsg 8738*	Closed form of elqs 8739. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅))
Theorem	elqs 8739*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsi 8740*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsecl 8741*	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 8742	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 8743	Membership of an equivalence class in a quotient set. More restrictive antecedent; kept for backward compatibility; for new work, prefer ecelqs 8742. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.) (Proof shortened by AV, 25-Nov-2025.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
Theorem	ecelqsi 8744	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 8745	"Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.)
⊢ 𝑅 ∈ V    &   ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅)    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [⟨𝐵, 𝐶⟩]𝑅 ∈ 𝑆)
Theorem	qsexg 8746	A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V)
Theorem	qsex 8747	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 / 𝑅) ∈ V
Theorem	uniqs 8748	The union of a quotient set, like uniqsw 8749 but with a weaker antecedent: only the restriction of 𝑅 by 𝐴 needs to be a set, not 𝑅 itself, see e.g. cnvepima 38796. (Contributed by NM, 9-Dec-2008.) (Revised by Peter Mazsa, 20-Jun-2019.)
⊢ ((𝑅 ↾ 𝐴) ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴))
Theorem	uniqsw 8749	The union of a quotient set. More restrictive antecedent; kept for backward compatibility; for new work, prefer uniqs 8748. (Contributed by NM, 9-Dec-2008.) (Proof shortened by AV, 25-Nov-2025.)
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴))
Theorem	qsss 8750	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 8751	The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴)
Theorem	snecg 8752	The singleton of a coset is the singleton quotient. (Contributed by Peter Mazsa, 25-Mar-2019.)
⊢ (𝐴 ∈ 𝑉 → {[𝐴]𝑅} = ({𝐴} / 𝑅))
Theorem	snec 8753	The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅)
Theorem	ecqs 8754	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
⊢ 𝑅 ∈ V    ⇒   ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅)
Theorem	ecid 8755	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 8756	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 8757*	Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑆 = (𝐵 / 𝑅)    &   ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑)    ⇒   ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓)
Theorem	ectocl 8758*	Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑆 = (𝐵 / 𝑅)    &   ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑆 → 𝜓)
Theorem	elqsn0 8759	A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995.)
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅)
Theorem	ecelqsdm 8760	Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.)
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴)
Theorem	ecelqsdmb 8761	𝑅-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 8762	𝑅-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 8763	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 8764*	The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵)
Theorem	riiner 8765*	The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ((𝐵 × 𝐵) ∩ ∩ 𝑥 ∈ 𝐴 𝑅) Er 𝐵)
Theorem	erinxp 8766	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 8767	Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴)))
Theorem	qsinxp 8768	Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴))))
Theorem	qsdisj 8769	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 8770*	A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.)
⊢ (𝑅 Er 𝑋 → Disj 𝑥 ∈ (𝐴 / 𝑅)𝑥)
Theorem	qsel 8771	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 8772	Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4886. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.)
⊢ 𝑅 Er 𝑋    ⇒   ⊢ ((𝐵 ⊆ (𝐴 / 𝑅) ∧ 𝐶 ⊆ (𝐴 / 𝑅)) → ∪ (𝐵 ∩ 𝐶) = (∪ 𝐵 ∩ ∪ 𝐶))
Theorem	qliftlem 8773*	Lemma for theorems about a function lift. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅))
Theorem	qliftrel 8774*	𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌))
Theorem	qliftel 8775*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴)))
Theorem	qliftel1 8776*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴)
Theorem	qliftfun 8777*	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 8778*	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 8779*	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 8780*	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 8781*	The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵)
Theorem	ecoptocl 8782*	Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.)
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅)    &   ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑆 → 𝜓)
Theorem	2ecoptocl 8783*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.)
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅)    &   ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒)
Theorem	3ecoptocl 8784*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.)
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅)    &   ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ([⟨𝑣, 𝑢⟩]𝑅 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃)
Theorem	brecop 8785*	Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.)
⊢ ∼ ∈ V    &   ⊢ ∼ Er (𝐺 × 𝐺)    &   ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ )    &   ⊢ ≤ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ∼ ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ∼ ) ∧ 𝜑))}    &   ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([⟨𝑧, 𝑤⟩] ∼ = [⟨𝐴, 𝐵⟩] ∼ ∧ [⟨𝑣, 𝑢⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) → (𝜑 ↔ 𝜓)))    ⇒   ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ ≤ [⟨𝐶, 𝐷⟩] ∼ ↔ 𝜓))
Theorem	brecop2 8786	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 8787*	Lemma for erov 8789 and eroprf 8790. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐽 = (𝐴 / 𝑅)    &   ⊢ 𝐾 = (𝐵 / 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑅 Er 𝑈)    &   ⊢ (𝜑 → 𝑆 Er 𝑉)    &   ⊢ (𝜑 → 𝑇 Er 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑊)    &   ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Theorem	erovlem 8788*	Lemma for erov 8789 and eroprf 8790. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ 𝐽 = (𝐴 / 𝑅)    &   ⊢ 𝐾 = (𝐵 / 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑅 Er 𝑈)    &   ⊢ (𝜑 → 𝑆 Er 𝑉)    &   ⊢ (𝜑 → 𝑇 Er 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑊)    &   ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)}    ⇒   ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))))
Theorem	erov 8789*	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 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑊)    &   ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)}    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵) → ([𝑃]𝑅 ⨣ [𝑄]𝑆) = [(𝑃 + 𝑄)]𝑇)
Theorem	eroprf 8790*	Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ 𝐽 = (𝐴 / 𝑅)    &   ⊢ 𝐾 = (𝐵 / 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑅 Er 𝑈)    &   ⊢ (𝜑 → 𝑆 Er 𝑉)    &   ⊢ (𝜑 → 𝑇 Er 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑊)    &   ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)}    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑌)    &   ⊢ 𝐿 = (𝐶 / 𝑇)    ⇒   ⊢ (𝜑 → ⨣ :(𝐽 × 𝐾)⟶𝐿)
Theorem	erov2 8791*	The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐽 = (𝐴 / ∼ )    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )}    &   ⊢ (𝜑 → ∼ ∈ 𝑋)    &   ⊢ (𝜑 → ∼ Er 𝑈)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢)))    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ([𝑃] ∼ ⨣ [𝑄] ∼ ) = [(𝑃 + 𝑄)] ∼ )
Theorem	eroprf2 8792*	Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐽 = (𝐴 / ∼ )    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )}    &   ⊢ (𝜑 → ∼ ∈ 𝑋)    &   ⊢ (𝜑 → ∼ Er 𝑈)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢)))    ⇒   ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽)
Theorem	ecopoveq 8793*	This is the first of several theorems about equivalence relations of the kind used in construction of fractions and signed reals, involving operations on equivalent classes of ordered pairs. This theorem expresses the relation ∼ (specified by the hypothesis) in terms of its operation 𝐹. (Contributed by NM, 16-Aug-1995.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}    ⇒   ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩ ∼ ⟨𝐶, 𝐷⟩ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))
Theorem	ecopovsym 8794*	Assuming the operation 𝐹 is commutative, show that the relation ∼, specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}    &   ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)    ⇒   ⊢ (𝐴 ∼ 𝐵 → 𝐵 ∼ 𝐴)
Theorem	ecopovtrn 8795*	Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation ∼, specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}    &   ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))    ⇒   ⊢ ((𝐴 ∼ 𝐵 ∧ 𝐵 ∼ 𝐶) → 𝐴 ∼ 𝐶)
Theorem	ecopover 8796*	Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation ∼, specified by the first hypothesis, is an equivalence relation. (Contributed by NM, 16-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof shortened by AV, 1-May-2021.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}    &   ⊢ (𝑥 + 𝑦) = (𝑦 + 𝑥)    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))    ⇒   ⊢ ∼ Er (𝑆 × 𝑆)
Theorem	eceqoveq 8797*	Equality of equivalence relation in terms of an operation. (Contributed by NM, 15-Feb-1996.) (Proof shortened by Mario Carneiro, 12-Aug-2015.)
⊢ ∼ Er (𝑆 × 𝑆)    &   ⊢ dom + = (𝑆 × 𝑆)    &   ⊢ ¬ ∅ ∈ 𝑆    &   ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩ ∼ ⟨𝐶, 𝐷⟩ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ([⟨𝐴, 𝐵⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))
Theorem	ecovcom 8798*	Lemma used to transfer a commutative law via an equivalence relation. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
⊢ 𝐶 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐷, 𝐺⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑥, 𝑦⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )    &   ⊢ 𝐷 = 𝐻    &   ⊢ 𝐺 = 𝐽    ⇒   ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	ecovass 8799*	Lemma used to transfer an associative law via an equivalence relation. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝐺, 𝐻⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑁, 𝑄⟩] ∼ )    &   ⊢ (((𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝐺, 𝐻⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝐽, 𝐾⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ + [⟨𝑁, 𝑄⟩] ∼ ) = [⟨𝐿, 𝑀⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝐺 ∈ 𝑆 ∧ 𝐻 ∈ 𝑆))    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑁 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆))    &   ⊢ 𝐽 = 𝐿    &   ⊢ 𝐾 = 𝑀    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Theorem	ecovdi 8800*	Lemma used to transfer a distributive law via an equivalence relation. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑀, 𝑁⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝑊, 𝑋⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑌, 𝑍⟩] ∼ )    &   ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ) = [⟨𝐾, 𝐿⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆))    &   ⊢ 𝐻 = 𝐾    &   ⊢ 𝐽 = 𝐿    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))