P. 371 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37001-37100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cosselcnvrefrels3 37001*	Necessary and sufficient condition for a coset relation to be an element of the converse reflexive relation class. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ ( ≀ 𝑅 ∈ CnvRefRels ↔ (∀𝑢∀𝑥∀𝑦((𝑢𝑅𝑥 ∧ 𝑢𝑅𝑦) → 𝑥 = 𝑦) ∧ ≀ 𝑅 ∈ Rels ))
Theorem	cosselcnvrefrels4 37002*	Necessary and sufficient condition for a coset relation to be an element of the converse reflexive relation class. (Contributed by Peter Mazsa, 31-Aug-2021.)
⊢ ( ≀ 𝑅 ∈ CnvRefRels ↔ (∀𝑢∃*𝑥 𝑢𝑅𝑥 ∧ ≀ 𝑅 ∈ Rels ))
Theorem	cosselcnvrefrels5 37003*	Necessary and sufficient condition for a coset relation to be an element of the converse reflexive relation class. (Contributed by Peter Mazsa, 5-Sep-2021.)
⊢ ( ≀ 𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ ran 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 ∨ ([𝑥]◡𝑅 ∩ [𝑦]◡𝑅) = ∅) ∧ ≀ 𝑅 ∈ Rels ))
21.22.9  Symmetry
Definition	df-syms 37004	Define the class of all symmetric sets. It is used only by df-symrels 37005. Note the similarity of Definitions df-refs 36972, df-syms 37004 and df-trs 37034, cf. the comment of dfrefrels2 36975. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-symrels 37005	Define the class of symmetric relations. For sets, being an element of the class of symmetric relations is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 37019. Alternate definitions are dfsymrels2 37007, dfsymrels3 37008, dfsymrels4 37009 and dfsymrels5 37010. This definition is similar to the definitions of the classes of reflexive (df-refrels 36973) and transitive (df-trrels 37035) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ SymRels = ( Syms ∩ Rels )
Definition	df-symrel 37006	Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 37005) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 37019. Alternate definitions are dfsymrel2 37011 and dfsymrel3 37012. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfsymrels2 37007	Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 36975. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}
Theorem	dfsymrels3 37008*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)}
Theorem	dfsymrels4 37009	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟}
Theorem	dfsymrels5 37010*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}
Theorem	dfsymrel2 37011	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 19-Apr-2019.) (Revised by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (◡𝑅 ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dfsymrel3 37012*	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 21-Apr-2019.) (Revised by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ Rel 𝑅))
Theorem	dfsymrel4 37013	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅))
Theorem	dfsymrel5 37014*	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅))
Theorem	elsymrels2 37015	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels3 37016*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels4 37017	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels5 37018*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrelsrel 37019	For sets, being an element of the class of symmetric relations (df-symrels 37005) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅))
Theorem	symreleq 37020	Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆))
Theorem	symrelim 37021	Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	symrelcoss 37022	The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.)
⊢ SymRel ≀ 𝑅
Theorem	idsymrel 37023	The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.)
⊢ SymRel I
Theorem	epnsymrel 37024	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ¬ SymRel E
21.22.10  Reflexivity and symmetry
Theorem	symrefref2 37025	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 37026. (Contributed by Peter Mazsa, 19-Jul-2018.)
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅))
Theorem	symrefref3 37026*	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 37025. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥))
Theorem	refsymrels2 37027	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 37050) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 36975, cf. the comment of dfrefrels2 36975. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
Theorem	refsymrels3 37028*	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 37051) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 36976, cf. the comment of dfrefrel3 36978. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))}
Theorem	refsymrel2 37029	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 36977, cf. the comment of dfrefrels2 36975. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅))
Theorem	refsymrel3 37030*	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 36978, cf. the comment of dfrefrel3 36978. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅))
Theorem	elrefsymrels2 37031	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 37050) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 36975, cf. the comment of dfrefrels2 36975. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrels3 37032*	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 37051) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 36976, cf. the comment of dfrefrel3 36978. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrelsrel 37033	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.22.11  Transitivity
Definition	df-trs 37034	Define the class of all transitive sets (versus the transitive class defined in df-tr 5223). It is used only by df-trrels 37035. Note the similarity of the definitions of df-refs 36972, df-syms 37004 and df-trs 37034. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-trrels 37035	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 37043. Alternate definitions are dftrrels2 37037 and dftrrels3 37038. This definition is similar to the definitions of the classes of reflexive (df-refrels 36973) and symmetric (df-symrels 37005) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ TrRels = ( Trs ∩ Rels )
Definition	df-trrel 37036	Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 37035) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 37043. Alternate definitions are dftrrel2 37039 and dftrrel3 37040. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dftrrels2 37037	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 5642 (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 36873 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 37038*	Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)}
Theorem	dftrrel2 37039	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dftrrel3 37040*	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅))
Theorem	eltrrels2 37041	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	eltrrels3 37042*	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels ))
Theorem	eltrrelsrel 37043	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 37044	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 37045	Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 36904) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024.)
⊢ TrRel (𝑅 ↾ {𝐴})
21.22.12  Equivalence relations
Definition	df-eqvrels 37046	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 37056. Alternate definitions are dfeqvrels2 37050 and dfeqvrels3 37051. (Contributed by Peter Mazsa, 7-Nov-2018.)
⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )
Definition	df-eqvrel 37047	Define the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) For sets, being an element of the class of equivalence relations (df-eqvrels 37046) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 37056. Alternate definitions are dfeqvrel2 37052 and dfeqvrel3 37053. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅))
Definition	df-coeleqvrels 37048	Define the 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 37058. Alternate definition is dfcoeleqvrels 37083. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ CoElEqvRels = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) ∈ EqvRels }
Definition	df-coeleqvrel 37049	Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.) Alternate definition is dfcoeleqvrel 37084. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 37058. (Contributed by Peter Mazsa, 11-Dec-2021.)
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴))
Theorem	dfeqvrels2 37050	Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.)
⊢ EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}
Theorem	dfeqvrels3 37051*	Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.)
⊢ EqvRels = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
Theorem	dfeqvrel2 37052	Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ Rel 𝑅))
Theorem	dfeqvrel3 37053*	Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ Rel 𝑅))
Theorem	eleqvrels2 37054	Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ EqvRels ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
Theorem	eleqvrels3 37055*	Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels ))
Theorem	eleqvrelsrel 37056	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 37057	Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ ≀ (◡ E ↾ 𝐴) ∈ EqvRels ))
Theorem	elcoeleqvrelsrel 37058	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 37059	An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.)
⊢ ( EqvRel 𝑅 → Rel 𝑅)
Theorem	eqvrelrefrel 37060	An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → RefRel 𝑅)
Theorem	eqvrelsymrel 37061	An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → SymRel 𝑅)
Theorem	eqvreltrrel 37062	An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → TrRel 𝑅)
Theorem	eqvrelim 37063	Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	eqvreleq 37064	Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvreleqi 37065	Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆)
Theorem	eqvreleqd 37066	Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvrelsym 37067	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 37068	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 37069	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 37070	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqvreltr4d 37071	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqvrelref 37072	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 37073	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 37074	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 37075	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 37076	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 37077	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 37078	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 37079	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020.) (Revised by Peter Mazsa, 20-Dec-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ TrRel ≀ 𝑅)
Theorem	eqvrelcoss3 37080*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 28-Apr-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≀ 𝑅𝑦 ∧ 𝑦 ≀ 𝑅𝑧) → 𝑥 ≀ 𝑅𝑧))
Theorem	eqvrelcoss2 37081	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.)
⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅)
Theorem	eqvrelcoss4 37082*	Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019.) (Revised by Peter Mazsa, 30-Sep-2021.)
⊢ ( EqvRel ≀ 𝑅 ↔ ∀𝑥∀𝑧(([𝑥] ≀ 𝑅 ∩ [𝑧] ≀ 𝑅) ≠ ∅ → ([𝑥]◡𝑅 ∩ [𝑧]◡𝑅) ≠ ∅))
Theorem	dfcoeleqvrels 37083	Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 37081, eqvrelcoss3 37080 and eqvrelcoss4 37082 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ CoElEqvRels = {𝑎 ∣ ∼ 𝑎 ∈ EqvRels }
Theorem	dfcoeleqvrel 37084	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 37081, eqvrelcoss3 37080 and eqvrelcoss4 37082 when needed. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴)
21.22.13  Redundancy
Definition	df-redunds 37085*	Define the class of all redundant sets 𝑥 with respect to 𝑦 in 𝑧. For sets, binary relation on the class of all redundant sets (brredunds 37088) is equivalent to satisfying the redundancy predicate (df-redund 37086). (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ Redunds = ◡{⟨⟨𝑦, 𝑧⟩, 𝑥⟩ ∣ (𝑥 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑧) = (𝑦 ∩ 𝑧))}
Definition	df-redund 37086	Define the redundancy predicate. Read: 𝐴 is redundant with respect to 𝐵 in 𝐶. For sets, binary relation on the class of all redundant sets (brredunds 37088) is equivalent to satisfying the redundancy predicate. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶)))
Definition	df-redundp 37087	Define the redundancy operator for propositions, cf. df-redund 37086. (Contributed by Peter Mazsa, 23-Oct-2022.)
⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))))
Theorem	brredunds 37088	Binary relation on the class of all redundant sets. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ (𝐴 ⊆ 𝐵 ∧ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))))
Theorem	brredundsredund 37089	For sets, binary relation on the class of all redundant sets (brredunds 37088) is equivalent to satisfying the redundancy predicate (df-redund 37086). (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 Redunds ⟨𝐵, 𝐶⟩ ↔ 𝐴 Redund ⟨𝐵, 𝐶⟩))
Theorem	redundss3 37090	Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ 𝐷 ⊆ 𝐶    ⇒   ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ → 𝐴 Redund ⟨𝐵, 𝐷⟩)
Theorem	redundeq1 37091	Equivalence of redundancy predicates. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ 𝐴 = 𝐷    ⇒   ⊢ (𝐴 Redund ⟨𝐵, 𝐶⟩ ↔ 𝐷 Redund ⟨𝐵, 𝐶⟩)
Theorem	redundpim3 37092	Implication of redundancy of proposition. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ (𝜃 → 𝜒)    ⇒   ⊢ ( redund (𝜑, 𝜓, 𝜒) → redund (𝜑, 𝜓, 𝜃))
Theorem	redundpbi1 37093	Equivalence of redundancy of propositions. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ (𝜑 ↔ 𝜃)    ⇒   ⊢ ( redund (𝜑, 𝜓, 𝜒) ↔ redund (𝜃, 𝜓, 𝜒))
Theorem	refrelsredund4 37094	The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 36975) if the relations are symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , ( RefRels ∩ SymRels )⟩
Theorem	refrelsredund2 37095	The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 36975) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ( I ↾ dom 𝑟) ⊆ 𝑟} Redund ⟨ RefRels , EqvRels ⟩
Theorem	refrelsredund3 37096*	The naive version of the class of reflexive relations {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥} is redundant with respect to the class of reflexive relations (see dfrefrels3 36976) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥} Redund ⟨ RefRels , EqvRels ⟩
Theorem	refrelredund4 37097	The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 36977) if the relation is symmetric as well. (Contributed by Peter Mazsa, 26-Oct-2022.)
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, ( RefRel 𝑅 ∧ SymRel 𝑅))
Theorem	refrelredund2 37098	The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 36977) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ redund ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅)
Theorem	refrelredund3 37099*	The naive version of the definition of reflexive relation (∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 ∧ Rel 𝑅) is redundant with respect to reflexive relation (see dfrefrel3 36978) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022.)
⊢ redund ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ Rel 𝑅), RefRel 𝑅, EqvRel 𝑅)
21.22.14  Domain quotients
Definition	df-dmqss 37100*	Define the class of domain quotients. Domain quotients are pairs of sets, typically a relation and a set, where the quotient (see df-qs 8654) of the relation on its domain is equal to the set. See comments of df-ers 37125 for the motivation for this definition. (Contributed by Peter Mazsa, 16-Apr-2019.)
⊢ DomainQss = {⟨𝑥, 𝑦⟩ ∣ (dom 𝑥 / 𝑥) = 𝑦}