P. 86 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8501-8600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	errn 8501	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 8502	An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴))
Theorem	erex 8503	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 8504	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 8505*	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 8506*	A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 8505, 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 8507*	Alternate proof of iseri 8506, avoiding the usage of mptru 1549 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	brdifun 8508	Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴)))
Theorem	swoer 8509*	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 8510*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
Theorem	swoord2 8511*	The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < ))    &   ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵))
Theorem	swoso 8512*	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 8513*	Lemma for eqer 8514. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.)
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)    &   ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝐴 = 𝐵}    ⇒   ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴)
Theorem	eqer 8514*	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 8515	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 8516	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 8517	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq1d 8518	Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)
Theorem	eceq2 8519	Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵)
Theorem	eceq2i 8520	Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ [𝐶]𝐴 = [𝐶]𝐵
Theorem	eceq2d 8521	Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵)
Theorem	elecg 8522	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	elec 8523	Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)
Theorem	relelec 8524	Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴))
Theorem	ecss 8525	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 8526	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 8527	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 8528	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 8529	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 8530	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 8531	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 8532	An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.)
⊢ [𝐴] I = {𝐴}
Theorem	qseq1 8533	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐴 / 𝐶) = (𝐵 / 𝐶))
Theorem	qseq2 8534	Equality theorem for quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐴 = 𝐵 → (𝐶 / 𝐴) = (𝐶 / 𝐵))
Theorem	qseq2i 8535	Equality theorem for quotient set, inference form. (Contributed by Peter Mazsa, 3-Jun-2021.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ (𝐶 / 𝐴) = (𝐶 / 𝐵)
Theorem	qseq2d 8536	Equality theorem for quotient set, deduction form. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 / 𝐴) = (𝐶 / 𝐵))
Theorem	qseq12 8537	Equality theorem for quotient set. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 / 𝐶) = (𝐵 / 𝐷))
Theorem	elqsg 8538*	Closed form of elqs 8539. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝐵 ∈ 𝑉 → (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅))
Theorem	elqs 8539*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐵 ∈ (𝐴 / 𝑅) ↔ ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsi 8540*	Membership in a quotient set. (Contributed by NM, 23-Jul-1995.)
⊢ (𝐵 ∈ (𝐴 / 𝑅) → ∃𝑥 ∈ 𝐴 𝐵 = [𝑥]𝑅)
Theorem	elqsecl 8541*	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	ecelqsg 8542	Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅))
Theorem	ecelqsi 8543	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 8544	"Closure" law for equivalence class of ordered pairs. (Contributed by NM, 25-Mar-1996.)
⊢ 𝑅 ∈ V    &   ⊢ 𝑆 = ((𝐴 × 𝐴) / 𝑅)    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → [⟨𝐵, 𝐶⟩]𝑅 ∈ 𝑆)
Theorem	qsexg 8545	A quotient set exists. (Contributed by FL, 19-May-2007.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 / 𝑅) ∈ V)
Theorem	qsex 8546	A quotient set exists. (Contributed by NM, 14-Aug-1995.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 / 𝑅) ∈ V
Theorem	uniqs 8547	The union of a quotient set. (Contributed by NM, 9-Dec-2008.)
⊢ (𝑅 ∈ 𝑉 → ∪ (𝐴 / 𝑅) = (𝑅 “ 𝐴))
Theorem	qsss 8548	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 8549	The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ (𝜑 → 𝑅 Er 𝐴)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∪ (𝐴 / 𝑅) = 𝐴)
Theorem	snec 8550	The singleton of an equivalence class. (Contributed by NM, 29-Jan-1999.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐴 ∈ V    ⇒   ⊢ {[𝐴]𝑅} = ({𝐴} / 𝑅)
Theorem	ecqs 8551	Equivalence class in terms of quotient set. (Contributed by NM, 29-Jan-1999.)
⊢ 𝑅 ∈ V    ⇒   ⊢ [𝐴]𝑅 = ∪ ({𝐴} / 𝑅)
Theorem	ecid 8552	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 8553	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 8554*	Implicit substitution of class for equivalence class. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑆 = (𝐵 / 𝑅)    &   ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐵) → 𝜑)    ⇒   ⊢ ((𝜒 ∧ 𝐴 ∈ 𝑆) → 𝜓)
Theorem	ectocl 8555*	Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝑆 = (𝐵 / 𝑅)    &   ⊢ ([𝑥]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 ∈ 𝐵 → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑆 → 𝜓)
Theorem	elqsn0 8556	A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995.)
⊢ ((dom 𝑅 = 𝐴 ∧ 𝐵 ∈ (𝐴 / 𝑅)) → 𝐵 ≠ ∅)
Theorem	ecelqsdm 8557	Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995.)
⊢ ((dom 𝑅 = 𝐴 ∧ [𝐵]𝑅 ∈ (𝐴 / 𝑅)) → 𝐵 ∈ 𝐴)
Theorem	xpider 8558	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 8559*	The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵)
Theorem	riiner 8560*	The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ((𝐵 × 𝐵) ∩ ∩ 𝑥 ∈ 𝐴 𝑅) Er 𝐵)
Theorem	erinxp 8561	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 8562	Restrict the relation in an equivalence class to a base set. (Contributed by Mario Carneiro, 10-Jul-2015.)
⊢ (((𝑅 “ 𝐴) ⊆ 𝐴 ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 = [𝐵](𝑅 ∩ (𝐴 × 𝐴)))
Theorem	qsinxp 8563	Restrict the equivalence relation in a quotient set to the base set. (Contributed by Mario Carneiro, 23-Feb-2015.)
⊢ ((𝑅 “ 𝐴) ⊆ 𝐴 → (𝐴 / 𝑅) = (𝐴 / (𝑅 ∩ (𝐴 × 𝐴))))
Theorem	qsdisj 8564	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 8565*	A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016.)
⊢ (𝑅 Er 𝑋 → Disj 𝑥 ∈ (𝐴 / 𝑅)𝑥)
Theorem	qsel 8566	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 8567	Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4871. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.)
⊢ 𝑅 Er 𝑋    ⇒   ⊢ ((𝐵 ⊆ (𝐴 / 𝑅) ∧ 𝐶 ⊆ (𝐴 / 𝑅)) → ∪ (𝐵 ∩ 𝐶) = (∪ 𝐵 ∩ ∪ 𝐶))
Theorem	qliftlem 8568*	Lemma for theorems about a function lift. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅 ∈ (𝑋 / 𝑅))
Theorem	qliftrel 8569*	𝐹, a function lift, is a subset of 𝑅 × 𝑆. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐹 ⊆ ((𝑋 / 𝑅) × 𝑌))
Theorem	qliftel 8570*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ([𝐶]𝑅𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶𝑅𝑥 ∧ 𝐷 = 𝐴)))
Theorem	qliftel1 8571*	Elementhood in the relation 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → [𝑥]𝑅𝐹𝐴)
Theorem	qliftfun 8572*	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 8573*	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 8574*	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 8575*	The domain and range of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (Fun 𝐹 ↔ 𝐹:(𝑋 / 𝑅)⟶𝑌))
Theorem	qliftval 8576*	The value of the function 𝐹. (Contributed by Mario Carneiro, 23-Dec-2016.) (Revised by AV, 3-Aug-2024.)
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ ⟨[𝑥]𝑅, 𝐴⟩)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 Er 𝑋)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝑥 = 𝐶 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → Fun 𝐹)    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → (𝐹‘[𝐶]𝑅) = 𝐵)
Theorem	ecoptocl 8577*	Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995.)
⊢ 𝑆 = ((𝐵 × 𝐶) / 𝑅)    &   ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) → 𝜑)    ⇒   ⊢ (𝐴 ∈ 𝑆 → 𝜓)
Theorem	2ecoptocl 8578*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 23-Jul-1995.)
⊢ 𝑆 = ((𝐶 × 𝐷) / 𝑅)    &   ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ (((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝜒)
Theorem	3ecoptocl 8579*	Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995.)
⊢ 𝑆 = ((𝐷 × 𝐷) / 𝑅)    &   ⊢ ([⟨𝑥, 𝑦⟩]𝑅 = 𝐴 → (𝜑 ↔ 𝜓))    &   ⊢ ([⟨𝑧, 𝑤⟩]𝑅 = 𝐵 → (𝜓 ↔ 𝜒))    &   ⊢ ([⟨𝑣, 𝑢⟩]𝑅 = 𝐶 → (𝜒 ↔ 𝜃))    &   ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷)) → 𝜑)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 𝜃)
Theorem	brecop 8580*	Binary relation on a quotient set. Lemma for real number construction. (Contributed by NM, 29-Jan-1996.)
⊢ ∼ ∈ V    &   ⊢ ∼ Er (𝐺 × 𝐺)    &   ⊢ 𝐻 = ((𝐺 × 𝐺) / ∼ )    &   ⊢ ≤ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ∼ ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ∼ ) ∧ 𝜑))}    &   ⊢ ((((𝑧 ∈ 𝐺 ∧ 𝑤 ∈ 𝐺) ∧ (𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺)) ∧ ((𝑣 ∈ 𝐺 ∧ 𝑢 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺))) → (([⟨𝑧, 𝑤⟩] ∼ = [⟨𝐴, 𝐵⟩] ∼ ∧ [⟨𝑣, 𝑢⟩] ∼ = [⟨𝐶, 𝐷⟩] ∼ ) → (𝜑 ↔ 𝜓)))    ⇒   ⊢ (((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐺) ∧ (𝐶 ∈ 𝐺 ∧ 𝐷 ∈ 𝐺)) → ([⟨𝐴, 𝐵⟩] ∼ ≤ [⟨𝐶, 𝐷⟩] ∼ ↔ 𝜓))
Theorem	brecop2 8581	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 8582*	Lemma for erov 8584 and eroprf 8585. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ 𝐽 = (𝐴 / 𝑅)    &   ⊢ 𝐾 = (𝐵 / 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑅 Er 𝑈)    &   ⊢ (𝜑 → 𝑆 Er 𝑉)    &   ⊢ (𝜑 → 𝑇 Er 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑊)    &   ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑋 = [𝑝]𝑅 ∧ 𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Theorem	erovlem 8583*	Lemma for erov 8584 and eroprf 8585. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 30-Dec-2014.)
⊢ 𝐽 = (𝐴 / 𝑅)    &   ⊢ 𝐾 = (𝐵 / 𝑆)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑍)    &   ⊢ (𝜑 → 𝑅 Er 𝑈)    &   ⊢ (𝜑 → 𝑆 Er 𝑉)    &   ⊢ (𝜑 → 𝑇 Er 𝑊)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑉)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝑊)    &   ⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)}    ⇒   ⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))))
Theorem	erov 8584*	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 8585*	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 8586*	The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐽 = (𝐴 / ∼ )    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )}    &   ⊢ (𝜑 → ∼ ∈ 𝑋)    &   ⊢ (𝜑 → ∼ Er 𝑈)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢)))    ⇒   ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ([𝑃] ∼ ⨣ [𝑄] ∼ ) = [(𝑃 + 𝑄)] ∼ )
Theorem	eroprf2 8587*	Functionality of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐽 = (𝐴 / ∼ )    &   ⊢ ⨣ = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ((𝑥 = [𝑝] ∼ ∧ 𝑦 = [𝑞] ∼ ) ∧ 𝑧 = [(𝑝 + 𝑞)] ∼ )}    &   ⊢ (𝜑 → ∼ ∈ 𝑋)    &   ⊢ (𝜑 → ∼ Er 𝑈)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑈)    &   ⊢ (𝜑 → + :(𝐴 × 𝐴)⟶𝐴)    &   ⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴))) → ((𝑟 ∼ 𝑠 ∧ 𝑡 ∼ 𝑢) → (𝑟 + 𝑡) ∼ (𝑠 + 𝑢)))    ⇒   ⊢ (𝜑 → ⨣ :(𝐽 × 𝐽)⟶𝐽)
Theorem	ecopoveq 8588*	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 8589*	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 8590*	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 8591*	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 8592*	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 8593*	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 8594*	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 8595*	Lemma used to transfer a distributive law via an equivalence relation. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑧, 𝑤⟩] ∼ + [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑀, 𝑁⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑧, 𝑤⟩] ∼ ) = [⟨𝑊, 𝑋⟩] ∼ )    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ([⟨𝑥, 𝑦⟩] ∼ · [⟨𝑣, 𝑢⟩] ∼ ) = [⟨𝑌, 𝑍⟩] ∼ )    &   ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ) = [⟨𝐾, 𝐿⟩] ∼ )    &   ⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆))    &   ⊢ (((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆))    &   ⊢ 𝐻 = 𝐾    &   ⊢ 𝐽 = 𝐿    ⇒   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
2.4.23  The mapping operation
Syntax	cmap 8596	Extend the definition of a class to include the mapping operation. (Read for 𝐴 ↑m 𝐵, "the set of all functions that map from 𝐵 to 𝐴.)
class ↑m
Syntax	cpm 8597	Extend the definition of a class to include the partial mapping operation. (Read for 𝐴 ↑pm 𝐵, "the set of all partial functions that map from 𝐵 to 𝐴.)
class ↑pm
Definition	df-map 8598*	Define the mapping operation or set exponentiation. The set of all functions that map from 𝐵 to 𝐴 is written (𝐴 ↑m 𝐵) (see mapval 8608). Many authors write 𝐴 followed by 𝐵 as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring] p. 95). Other authors show 𝐵 as a prefixed superscript, which is read "𝐴 pre 𝐵 " (e.g., definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(𝐵, 𝐴) for our (𝐴 ↑m 𝐵). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003.)
⊢ ↑m = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∣ 𝑓:𝑦⟶𝑥})
Definition	df-pm 8599*	Define the partial mapping operation. A partial function from 𝐵 to 𝐴 is a function from a subset of 𝐵 to 𝐴. The set of all partial functions from 𝐵 to 𝐴 is written (𝐴 ↑pm 𝐵) (see pmvalg 8607). A notation for this operation apparently does not appear in the literature. We use ↑pm to distinguish it from the less general set exponentiation operation ↑m (df-map 8598). See mapsspm 8645 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓})
Theorem	mapprc 8600*	When 𝐴 is a proper class, the class of all functions mapping 𝐴 to 𝐵 is empty. Exercise 4.41 of [Mendelson] p. 255. (Contributed by NM, 8-Dec-2003.)
⊢ (¬ 𝐴 ∈ V → {𝑓 ∣ 𝑓:𝐴⟶𝐵} = ∅)