P. 392 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39101-39200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	symreleq 39101	Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆))
Theorem	symrelim 39102	Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	symrelcoss 39103	The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.)
⊢ SymRel ≀ 𝑅
Theorem	idsymrel 39104	The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.)
⊢ SymRel I
Theorem	epnsymrel 39105	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ¬ SymRel E
21.26.12  Reflexivity and symmetry
Theorem	symrefref2 39106	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 39107. (Contributed by Peter Mazsa, 19-Jul-2018.)
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅))
Theorem	symrefref3 39107*	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 39106. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥))
Theorem	refsymrels2 39108	Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels2 39131) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 39052, cf. the comment of dfrefrels2 39052. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
Theorem	refsymrels3 39109*	Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 39132) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 39053, cf. the comment of dfrefrel3 39055. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))}
Theorem	refsymrel2 39110	A relation which is reflexive and symmetric (like an equivalence relation) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrel2 39054, cf. the comment of dfrefrels2 39052. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅))
Theorem	refsymrel3 39111*	A relation which is reflexive and symmetric (like an equivalence relation) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for its reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrel3 39055, cf. the comment of dfrefrel3 39055. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅))
Theorem	elrefsymrels2 39112	Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels2 39131) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 39052, cf. the comment of dfrefrels2 39052. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrels3 39113*	Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 39132) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 39053, cf. the comment of dfrefrel3 39055. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrelsrel 39114	For sets, being an element of the class of reflexive and symmetric relations is equivalent to satisfying the reflexive and symmetric relation predicates. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ( RefRel 𝑅 ∧ SymRel 𝑅)))
21.26.13  Transitivity
Definition	df-trs 39115	Define the class of all transitive sets (versus the transitive class defined in df-tr 5205). It is used only by df-trrels 39116. Note the similarity of the definitions of df-refs 39049, df-syms 39081 and df-trs 39115. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-trrels 39116	Define the class of transitive relations. For sets, being an element of the class of transitive relations is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 39124. Alternate definitions are dftrrels2 39118 and dftrrels3 39119. This definition is similar to the definitions of the classes of reflexive (df-refrels 39050) and symmetric (df-symrels 39082) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ TrRels = ( Trs ∩ Rels )
Definition	df-trrel 39117	Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 39116) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 39124. Alternate definitions are dftrrel2 39120 and dftrrel3 39121. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dftrrels2 39118	Alternate definition of the class of transitive relations. I'd prefer to define the class of transitive relations by using the definition of composition by [Suppes] p. 63. df-coSUP (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐴𝑢 ∧ 𝑢𝐵𝑦)} as opposed to the present definition of composition df-co 5652 (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} because the Suppes definition keeps the order of 𝐴, 𝐵, 𝐶, 𝑅, 𝑆, 𝑇 by default in trsinxpSUP (((𝑅 ∩ (𝐴 × 𝐵)) ∘ (𝑆 ∩ (𝐵 × 𝐶))) ⊆ (𝑇 ∩ (𝐴 × 𝐶)) ↔ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵∀ 𝑧 ∈ 𝐶((𝑥𝑅𝑦 ∧ 𝑦𝑆𝑧) → 𝑥𝑇𝑧)) while the present definition of composition disarranges them: trsinxp (((𝑆 ∩ (𝐵 × 𝐶)) ∘ (𝑅 ∩ (𝐴 × 𝐵))) ⊆ (𝑇 ∩ (𝐴 × 𝐶 )) ↔ ∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐵∀𝑧 ∈ 𝐶((𝑥𝑅𝑦 ∧ 𝑦𝑆𝑧) → 𝑥𝑇𝑧) ). This is not mission critical to me, the implication of the Suppes definition is just more aesthetic, at least in the above case. If we swap to the Suppes definition of class composition, I would define the present class of all transitive sets as df-trsSUP and I would consider to switch the definition of the class of cosets by 𝑅 from the present df-coss 38960 to a df-cossSUP. But perhaps there is a mathematical reason to keep the present definition of composition. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ TrRels = {𝑟 ∈ Rels ∣ (𝑟 ∘ 𝑟) ⊆ 𝑟}
Theorem	dftrrels3 39119*	Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)}
Theorem	dftrrel2 39120	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dftrrel3 39121*	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅))
Theorem	eltrrels2 39122	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	eltrrels3 39123*	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels ))
Theorem	eltrrelsrel 39124	For sets, being an element of the class of transitive relations is equivalent to satisfying the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ TrRels ↔ TrRel 𝑅))
Theorem	trreleq 39125	Equality theorem for the transitive relation predicate. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( TrRel 𝑅 ↔ TrRel 𝑆))
Theorem	trrelressn 39126	Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38991) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024.)
⊢ TrRel (𝑅 ↾ {𝐴})
21.26.14  Equivalence relations
Definition	df-eqvrels 39127	Define the class of equivalence relations. For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 39137. Alternate definitions are dfeqvrels2 39131 and dfeqvrels3 39132. (Contributed by Peter Mazsa, 7-Nov-2018.)
⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )
Definition	df-eqvrel 39128	Define the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) For sets, being an element of the class of equivalence relations (df-eqvrels 39127) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 39137. Alternate definitions are dfeqvrel2 39133 and dfeqvrel3 39134. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅))
Definition	df-coeleqvrels 39129	Define the coelement equivalence relations class, the class of sets with coelement equivalence relations. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 39139. Alternate definition is dfcoeleqvrels 39164. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ CoElEqvRels = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) ∈ EqvRels }
Definition	df-coeleqvrel 39130	Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.) Alternate definition is dfcoeleqvrel 39165. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 39139. (Contributed by Peter Mazsa, 11-Dec-2021.)
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴))
Theorem	dfeqvrels2 39131	Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.)
⊢ EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}
Theorem	dfeqvrels3 39132*	Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.)
⊢ EqvRels = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
Theorem	dfeqvrel2 39133	Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ Rel 𝑅))
Theorem	dfeqvrel3 39134*	Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ Rel 𝑅))
Theorem	eleqvrels2 39135	Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ EqvRels ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
Theorem	eleqvrels3 39136*	Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels ))
Theorem	eleqvrelsrel 39137	For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ EqvRels ↔ EqvRel 𝑅))
Theorem	elcoeleqvrels 39138	Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ ≀ (◡ E ↾ 𝐴) ∈ EqvRels ))
Theorem	elcoeleqvrelsrel 39139	For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate. (Contributed by Peter Mazsa, 24-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ CoElEqvRel 𝐴))
Theorem	eqvrelrel 39140	An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.)
⊢ ( EqvRel 𝑅 → Rel 𝑅)
Theorem	eqvrelrefrel 39141	An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → RefRel 𝑅)
Theorem	eqvrelsymrel 39142	An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → SymRel 𝑅)
Theorem	eqvreltrrel 39143	An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → TrRel 𝑅)
Theorem	eqvrelim 39144	Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	eqvreleq 39145	Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvreleqi 39146	Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆)
Theorem	eqvreleqd 39147	Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvrelsym 39148	An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐵𝑅𝐴)
Theorem	eqvrelsymb 39149	An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised and distinct variable conditions removed by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴))
Theorem	eqvreltr 39150	An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    ⇒   ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
Theorem	eqvreltrd 39151	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqvreltr4d 39152	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqvrelref 39153	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.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐴)
Theorem	eqvrelth 39154	Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)    ⇒   ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Theorem	eqvrelcl 39155	Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ dom 𝑅)
Theorem	eqvrelthi 39156	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.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    ⇒   ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅)
Theorem	eqvreldisj 39157	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.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ ( EqvRel 𝑅 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅))
Theorem	qsdisjALTV 39158	Elements of a quotient set do not overlap. (Contributed by Rodolfo Medina, 12-Oct-2010.) (Revised by Mario Carneiro, 11-Jul-2014.) (Revised by Peter Mazsa, 3-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴 / 𝑅))    &   ⊢ (𝜑 → 𝐶 ∈ (𝐴 / 𝑅))    ⇒   ⊢ (𝜑 → (𝐵 = 𝐶 ∨ (𝐵 ∩ 𝐶) = ∅))
Theorem	eqvrelqsel 39159	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.) (Revised by Peter Mazsa, 28-Dec-2019.)
⊢ (( EqvRel 𝑅 ∧ 𝐵 ∈ (𝐴 / 𝑅) ∧ 𝐶 ∈ 𝐵) → 𝐵 = [𝐶]𝑅)
Theorem	eqvrelcoss 39160	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅)
Theorem	eqvrelcoss3 39161*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eqvrelcoss2 39162	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅)
Theorem	eqvrelcoss4 39163*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
Theorem	dfcoeleqvrels 39164	Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 39162, eqvrelcoss3 39161 and eqvrelcoss4 39163 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ CoElEqvRels = {𝑎 ∣ ∼ 𝑎 ∈ EqvRels }
Theorem	dfcoeleqvrel 39165	Alternate definition of the coelement equivalence relation predicate: a coelement equivalence relation is an equivalence relation on coelements. Other alternate definitions should be based on eqvrelcoss2 39162, eqvrelcoss3 39161 and eqvrelcoss4 39163 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴)
21.26.15  Redundancy
Definition	df-redunds 39166*	Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 39169) is equivalent to satisfying the redundancy predicate (df-redund 39167). (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}
Definition	df-redund 39167	Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 39169) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))
Definition	df-redundp 39168	Define the redundancy operator for propositions, cf. df-redund 39167. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))))
Theorem	brredunds 39169	Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))))
Theorem	brredundsredund 39170	For sets, binary relation on the class of all redundant sets (brredunds 39169) is equivalent to satisfying the redundancy predicate (df-redund 39167). (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ 𝐴 Redund ⟨𝐵, 𝐶⟩))
Theorem	redundss3 39171	Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ 𝐷 ⊆ 𝐶    ⇒   ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ → 𝐴 Redund ⟨𝐵, 𝐷⟩)
Theorem	redundeq1 39172	Equivalence of redundancy predicates. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ 𝐴 = 𝐷    ⇒   ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ 𝐷 Redund ⟨𝐵, 𝐶⟩)
Theorem	redundpim3 39173	Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ (𝜃 → 𝜒)    ⇒   ⊢ ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃))
Theorem	redundpbi1 39174	Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ (𝜑 ↔ 𝜃)    ⇒   ⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ redund (𝜃, 𝜓, 𝜒))
Theorem	refrelsredund4 39175	The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 39052) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , ( RefRels ∩ SymRels )⟩
Theorem	refrelsredund2 39176	The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 39052) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , EqvRels ⟩
Theorem	refrelsredund3 39177*	The naive version of the class of reflexive relations {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥} is redundant with respect to the class of reflexive relations (see dfrefrels3 39053) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥} Redund ⟨ RefRels , EqvRels ⟩
Theorem	refrelredund4 39178	The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 39054) if the relation is symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, ( RefRel 𝑅 ∧ SymRel 𝑅))
Theorem	refrelredund2 39179	The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 39054) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅)
Theorem	refrelredund3 39180*	The naive version of the definition of reflexive relation (∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 ∧ Rel 𝑅) is redundant with respect to reflexive relation (see dfrefrel3 39055) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ redund ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅)
21.26.16  Domain quotients
Definition	df-dmqss 39181*	Define the class of domain quotients. Domain quotients are pairs of sets, typically a relation and a set, where the quotient (see df-qs 8677) of the relation on its domain is equal to the set. See comments of df-ers 39207 for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019.)
⊢ DomainQss = {⟨𝑥, 𝑦⟩ ∣ (dom 𝑥 / 𝑥) = 𝑦}
Definition	df-dmqs 39182	Define the domain quotient predicate. (Read: the domain quotient of 𝑅 is 𝐴.) If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same, see brdmqssqs 39190. (Contributed by Peter Mazsa, 9-Aug-2021.)
⊢ (𝑅 DomainQs 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴)
Theorem	dmqseq 39183	Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝑅 = 𝑆 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆))
Theorem	dmqseqi 39184	Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆)
Theorem	dmqseqd 39185	Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → (dom 𝑅 / 𝑅) = (dom 𝑆 / 𝑆))
Theorem	dmqseqeq1 39186	Equality theorem for domain quotient. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ (𝑅 = 𝑆 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴))
Theorem	dmqseqeq1i 39187	Equality theorem for domain quotient, inference version. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴)
Theorem	dmqseqeq1d 39188	Equality theorem for domain quotient set, deduction version. (Contributed by Peter Mazsa, 26-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → ((dom 𝑅 / 𝑅) = 𝐴 ↔ (dom 𝑆 / 𝑆) = 𝐴))
Theorem	brdmqss 39189	The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ (dom 𝑅 / 𝑅) = 𝐴))
Theorem	brdmqssqs 39190	If 𝐴 and 𝑅 are sets, the domain quotient binary relation and the domain quotient predicate are the same. (Contributed by Peter Mazsa, 14-Aug-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊) → (𝑅 DomainQss 𝐴 ↔ 𝑅 DomainQs 𝐴))
Theorem	n0eldmqs 39191	The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018.)
⊢ ¬ ∅ ∈ (dom 𝑅 / 𝑅)
Theorem	qseq 39192*	The quotient set equal to a class. This theorem is used when a class 𝐴 is identified with a quotient (dom 𝑅 / 𝑅). In such a situation, every element 𝑢 ∈ 𝐴 is an 𝑅-coset [𝑣]𝑅 for some 𝑣 ∈ dom 𝑅, but there is no requirement that the "witness" 𝑣 be equal to its own block [𝑣]𝑅. 𝐴 is a set of blocks (equivalence classes), not a set of raw witnesses. In particular, when (dom 𝑅 / 𝑅) = 𝐴 is read together with a partition hypothesis 𝑅 Part 𝐴 (defined as dfpart2 39331), 𝐴 is being treated as the set of blocks [𝑣]𝑅; it does not assert any fixed-point condition 𝑣 = [𝑣]𝑅 such as would arise from the mistaken reading 𝑢 ∈ 𝐴 ↔ 𝑢 = [𝑢]𝑅. Cf. dmqsblocks 39426. (Contributed by Peter Mazsa, 19-Oct-2018.)
⊢ ((𝐵 / 𝑅) = 𝐴 ↔ ∀𝑢(𝑢 ∈ 𝐴 ↔ ∃𝑣 ∈ 𝐵 𝑢 = [𝑣]𝑅))
Theorem	n0eldmqseq 39193	The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 3-Nov-2018.)
⊢ ((dom 𝑅 / 𝑅) = 𝐴 → ¬ ∅ ∈ 𝐴)
Theorem	n0elim 39194	Implication of that the empty set is not an element of a class. (Contributed by Peter Mazsa, 30-Dec-2024.)
⊢ (¬ ∅ ∈ 𝐴 → (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴)
Theorem	n0el3 39195	Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 27-May-2021.)
⊢ (¬ ∅ ∈ 𝐴 ↔ (dom (◡ E ↾ 𝐴) / (◡ E ↾ 𝐴)) = 𝐴)
Theorem	cnvepresdmqss 39196	The domain quotient binary relation of the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021.)
⊢ (𝐴 ∈ 𝑉 → ((◡ E ↾ 𝐴) DomainQss 𝐴 ↔ ¬ ∅ ∈ 𝐴))
Theorem	cnvepresdmqs 39197	The domain quotient predicate for the restricted converse epsilon relation is equivalent to the negated elementhood of the empty set in the restriction. (Contributed by Peter Mazsa, 14-Aug-2021.)
⊢ ((◡ E ↾ 𝐴) DomainQs 𝐴 ↔ ¬ ∅ ∈ 𝐴)
Theorem	unidmqs 39198	The range of a relation is equal to the union of the domain quotient. (Contributed by Peter Mazsa, 13-Oct-2018.)
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ∪ (dom 𝑅 / 𝑅) = ran 𝑅))
Theorem	unidmqseq 39199	The union of the domain quotient of a relation is equal to the class 𝐴 if and only if the range is equal to it as well. (Contributed by Peter Mazsa, 21-Apr-2019.) (Revised by Peter Mazsa, 28-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → (∪ (dom 𝑅 / 𝑅) = 𝐴 ↔ ran 𝑅 = 𝐴)))
Theorem	dmqseqim 39200	If the domain quotient of a relation is equal to the class 𝐴, then the range of the relation is the union of the class. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ (𝑅 ∈ 𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → ran 𝑅 = ∪ 𝐴)))