P. 386 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38501-38600   *Has distinct variable group(s)

Type	Label	Description
Statement
21.26.7  Reflexivity
Definition	df-refs 38501	Define the class of all reflexive sets. It is used only by df-refrels 38502. We use subset relation S (df-ssr 38489) here to be able to define converse reflexivity (df-cnvrefs 38516), see also the comment of df-ssr 38489. The elements of this class are not necessarily relations (versus df-refrels 38502). Note the similarity of Definitions df-refs 38501, df-syms 38533 and df-trs 38563, cf. comments of dfrefrels2 38504. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Refs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-refrels 38502	Define the class of reflexive relations. This is practically dfrefrels2 38504 (which reveals that RefRels can not include proper classes like I as is elements, see comments of dfrefrels2 38504). Another alternative definition is dfrefrels3 38505. The element of this class and the reflexive relation predicate (df-refrel 38503) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, see elrefrelsrel 38511. This definition is similar to the definitions of the classes of symmetric (df-symrels 38534) and transitive (df-trrels 38564) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ RefRels = ( Refs ∩ Rels )
Definition	df-refrel 38503	Define the reflexive relation predicate. (Read: 𝑅 is a reflexive relation.) This is a surprising definition, see the comment of dfrefrel3 38507. Alternate definitions are dfrefrel2 38506 and dfrefrel3 38507. For sets, being an element of the class of reflexive relations (df-refrels 38502) is equivalent to satisfying the reflexive relation predicate, that is (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝑅 is a set, see elrefrelsrel 38511. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfrefrels2 38504	Alternate definition of the class of reflexive relations. This is a 0-ary class constant, which is recommended for definitions (see the 1. Guideline at https://us.metamath.org/ileuni/mathbox.html). Proper classes (like I, see iprc 7887) are not elements of this (or any) class: if a class is an element of another class, it is not a proper class but a set, see elex 3468. So if we use 0-ary constant classes as our main definitions, they are valid only for sets, not for proper classes. For proper classes we use predicate-type definitions like df-refrel 38503. See also the comment of df-rels 38476. Note that while elementhood in the class of relations cancels restriction of 𝑟 in dfrefrels2 38504, it keeps restriction of I: this is why the very similar definitions df-refs 38501, df-syms 38533 and df-trs 38563 diverge when we switch from (general) sets to relations in dfrefrels2 38504, dfsymrels2 38536 and dftrrels2 38566. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ RefRels = {𝑟 ∈ Rels ∣ ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟}
Theorem	dfrefrels3 38505*	Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ RefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦)}
Theorem	dfrefrel2 38506	Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ ( RefRel 𝑅 ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dfrefrel3 38507*	Alternate definition of the reflexive relation predicate. A relation is reflexive iff: for all elements on its domain and range, if an element of its domain is the same as an element of its range, then there is the relation between them. Note that this is definitely not the definition we are accustomed to, like e.g. idref 7118 / idrefALT 6084 or df-reflexive 49757 ⊢ (𝑅Reflexive𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥)). It turns out that the not-surprising definition which contains ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 needs symmetry as well, see refsymrels3 38557. Only when this symmetry condition holds, like in case of equivalence relations, see dfeqvrels3 38580, can we write the traditional form ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 for reflexive relations. For the special case with square Cartesian product when the two forms are equivalent see idinxpssinxp4 38308 where ⊢ (∀𝑥 ∈ 𝐴∀𝑦 ∈ 𝐴(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ 𝐴𝑥𝑅𝑥). See also similar definition of the converse reflexive relations class dfcnvrefrel3 38522. (Contributed by Peter Mazsa, 8-Jul-2019.)
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ Rel 𝑅))
Theorem	dfrefrel5 38508*	Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 12-Dec-2023.)
⊢ ( RefRel 𝑅 ↔ (∀𝑥 ∈ (dom 𝑅 ∩ ran 𝑅)𝑥𝑅𝑥 ∧ Rel 𝑅))
Theorem	elrefrels2 38509	Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.)
⊢ (𝑅 ∈ RefRels ↔ (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elrefrels3 38510*	Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019.)
⊢ (𝑅 ∈ RefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ∧ 𝑅 ∈ Rels ))
Theorem	elrefrelsrel 38511	For sets, being an element of the class of reflexive relations (df-refrels 38502) is equivalent to satisfying the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ RefRels ↔ RefRel 𝑅))
Theorem	refreleq 38512	Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( RefRel 𝑅 ↔ RefRel 𝑆))
Theorem	refrelid 38513	Identity relation is reflexive. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ RefRel I
Theorem	refrelcoss 38514	The class of cosets by 𝑅 is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020.)
⊢ RefRel ≀ 𝑅
Theorem	refrelressn 38515	Any class ' R ' restricted to the singleton of the set ' A ' (see ressn2 38433) is reflexive. (Contributed by Peter Mazsa, 12-Jun-2024.)
⊢ (𝐴 ∈ 𝑉 → RefRel (𝑅 ↾ {𝐴}))
21.26.8  Converse reflexivity
Definition	df-cnvrefs 38516	Define the class of all converse reflexive sets, see the comment of df-ssr 38489. It is used only by df-cnvrefrels 38517. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ CnvRefs = {𝑥 ∣ ( I ∩ (dom 𝑥 × ran 𝑥))◡ S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-cnvrefrels 38517	Define the class of converse reflexive relations. This is practically dfcnvrefrels2 38519 (which uses the traditional subclass relation ⊆) : we use converse subset relation (brcnvssr 38497) here to ensure the comparability to the definitions of the classes of all reflexive (df-ref 23392), symmetric (df-syms 38533) and transitive (df-trs 38563) sets. We use this concept to define functions (df-funsALTV 38673, df-funALTV 38674) and disjoints (df-disjs 38696, df-disjALTV 38697). For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38527. Alternate definitions are dfcnvrefrels2 38519 and dfcnvrefrels3 38520. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ CnvRefRels = ( CnvRefs ∩ Rels )
Definition	df-cnvrefrel 38518	Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 38522. Alternate definitions are dfcnvrefrel2 38521 and dfcnvrefrel3 38522. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfcnvrefrels2 38519	Alternate definition of the class of converse reflexive relations. See the comment of dfrefrels2 38504. (Contributed by Peter Mazsa, 21-Jul-2021.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ 𝑟 ⊆ ( I ∩ (dom 𝑟 × ran 𝑟))}
Theorem	dfcnvrefrels3 38520*	Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ CnvRefRels = {𝑟 ∈ Rels ∣ ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥𝑟𝑦 → 𝑥 = 𝑦)}
Theorem	dfcnvrefrel2 38521	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfcnvrefrel3 38522*	Alternate definition of the converse reflexive relation predicate. A relation is converse reflexive iff: for all elements on its domain and range, if for an element of its domain and for an element of its range there is the relation between them, then the two elements are the same, cf. the comment of dfrefrel3 38507. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	dfcnvrefrel4 38523	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (𝑅 ⊆ I ∧ Rel 𝑅))
Theorem	dfcnvrefrel5 38524*	Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024.)
⊢ ( CnvRefRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ Rel 𝑅))
Theorem	elcnvrefrels2 38525	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019.)
⊢ (𝑅 ∈ CnvRefRels ↔ (𝑅 ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrels3 38526*	Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021.)
⊢ (𝑅 ∈ CnvRefRels ↔ (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥𝑅𝑦 → 𝑥 = 𝑦) ∧ 𝑅 ∈ Rels ))
Theorem	elcnvrefrelsrel 38527	For sets, being an element of the class of converse reflexive relations (df-cnvrefrels 38517) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ CnvRefRels ↔ CnvRefRel 𝑅))
Theorem	cnvrefrelcoss2 38528	Necessary and sufficient condition for a coset relation to be a converse reflexive relation. (Contributed by Peter Mazsa, 27-Jul-2021.)
⊢ ( CnvRefRel ≀ 𝑅 ↔ ≀ 𝑅 ⊆ I )
Theorem	cosselcnvrefrels2 38529	Necessary and sufficient condition for a coset relation to be an element of the converse reflexive relation class. (Contributed by Peter Mazsa, 25-Aug-2021.)
⊢ ( ≀ 𝑅 ∈ CnvRefRels ↔ ( ≀ 𝑅 ⊆ I ∧ ≀ 𝑅 ∈ Rels ))
Theorem	cosselcnvrefrels3 38530*	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 38531*	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 38532*	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.26.9  Symmetry
Definition	df-syms 38533	Define the class of all symmetric sets. It is used only by df-symrels 38534. Note the similarity of Definitions df-refs 38501, df-syms 38533 and df-trs 38563, cf. the comment of dfrefrels2 38504. (Contributed by Peter Mazsa, 19-Jul-2019.)
⊢ Syms = {𝑥 ∣ ◡(𝑥 ∩ (dom 𝑥 × ran 𝑥)) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-symrels 38534	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 38548. Alternate definitions are dfsymrels2 38536, dfsymrels3 38537, dfsymrels4 38538 and dfsymrels5 38539. This definition is similar to the definitions of the classes of reflexive (df-refrels 38502) and transitive (df-trrels 38564) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ SymRels = ( Syms ∩ Rels )
Definition	df-symrel 38535	Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 38534) is equivalent to satisfying the symmetric relation predicate, see elsymrelsrel 38548. Alternate definitions are dfsymrel2 38540 and dfsymrel3 38541. (Contributed by Peter Mazsa, 16-Jul-2021.)
⊢ ( SymRel 𝑅 ↔ (◡(𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dfsymrels2 38536	Alternate definition of the class of symmetric relations. Cf. the comment of dfrefrels2 38504. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 ⊆ 𝑟}
Theorem	dfsymrels3 38537*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥)}
Theorem	dfsymrels4 38538	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ◡𝑟 = 𝑟}
Theorem	dfsymrels5 38539*	Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ SymRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦(𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}
Theorem	dfsymrel2 38540	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 38541*	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 38542	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (◡𝑅 = 𝑅 ∧ Rel 𝑅))
Theorem	dfsymrel5 38543*	Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ ( SymRel 𝑅 ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ Rel 𝑅))
Theorem	elsymrels2 38544	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels3 38545*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels4 38546	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (◡𝑅 = 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	elsymrels5 38547*	Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ SymRels ↔ (∀𝑥∀𝑦(𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥) ∧ 𝑅 ∈ Rels ))
Theorem	elsymrelsrel 38548	For sets, being an element of the class of symmetric relations (df-symrels 38534) is equivalent to satisfying the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021.)
⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ SymRels ↔ SymRel 𝑅))
Theorem	symreleq 38549	Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆))
Theorem	symrelim 38550	Symmetric relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	symrelcoss 38551	The class of cosets by 𝑅 is symmetric. (Contributed by Peter Mazsa, 20-Dec-2021.)
⊢ SymRel ≀ 𝑅
Theorem	idsymrel 38552	The identity relation is symmetric. (Contributed by AV, 19-Jun-2022.)
⊢ SymRel I
Theorem	epnsymrel 38553	The membership (epsilon) relation is not symmetric. (Contributed by AV, 18-Jun-2022.)
⊢ ¬ SymRel E
21.26.10  Reflexivity and symmetry
Theorem	symrefref2 38554	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref3 38555. (Contributed by Peter Mazsa, 19-Jul-2018.)
⊢ (◡𝑅 ⊆ 𝑅 → (( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 ↔ ( I ↾ dom 𝑅) ⊆ 𝑅))
Theorem	symrefref3 38555*	Symmetry is a sufficient condition for the equivalence of two versions of the reflexive relation, see also symrefref2 38554. (Contributed by Peter Mazsa, 23-Aug-2021.) (Proof modification is discouraged.)
⊢ (∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥))
Theorem	refsymrels2 38556	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 38579) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑟 × ran 𝑟)) ⊆ 𝑟 version of dfrefrels2 38504, cf. the comment of dfrefrels2 38504. (Contributed by Peter Mazsa, 20-Jul-2019.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟)}
Theorem	refsymrels3 38557*	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 38580) can use the ∀𝑥 ∈ dom 𝑟𝑥𝑟𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑟∀𝑦 ∈ ran 𝑟(𝑥 = 𝑦 → 𝑥𝑟𝑦) version of dfrefrels3 38505, cf. the comment of dfrefrel3 38507. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ ( RefRels ∩ SymRels ) = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥))}
Theorem	refsymrel2 38558	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 38506, cf. the comment of dfrefrels2 38504. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ Rel 𝑅))
Theorem	refsymrel3 38559*	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 38507, cf. the comment of dfrefrel3 38507. (Contributed by Peter Mazsa, 23-Aug-2021.)
⊢ (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ Rel 𝑅))
Theorem	elrefsymrels2 38560	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 38579) can use the restricted version for their reflexive part (see below), not just the ( I ∩ (dom 𝑅 × ran 𝑅)) ⊆ 𝑅 version of dfrefrels2 38504, cf. the comment of dfrefrels2 38504. (Contributed by Peter Mazsa, 22-Jul-2019.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrels3 38561*	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 38580) can use the ∀𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for their reflexive part, not just the ∀𝑥 ∈ dom 𝑅∀𝑦 ∈ ran 𝑅(𝑥 = 𝑦 → 𝑥𝑅𝑦) version of dfrefrels3 38505, cf. the comment of dfrefrel3 38507. (Contributed by Peter Mazsa, 22-Jul-2019.) (Proof modification is discouraged.)
⊢ (𝑅 ∈ ( RefRels ∩ SymRels ) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ 𝑅 ∈ Rels ))
Theorem	elrefsymrelsrel 38562	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.11  Transitivity
Definition	df-trs 38563	Define the class of all transitive sets (versus the transitive class defined in df-tr 5215). It is used only by df-trrels 38564. Note the similarity of the definitions of df-refs 38501, df-syms 38533 and df-trs 38563. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ Trs = {𝑥 ∣ ((𝑥 ∩ (dom 𝑥 × ran 𝑥)) ∘ (𝑥 ∩ (dom 𝑥 × ran 𝑥))) S (𝑥 ∩ (dom 𝑥 × ran 𝑥))}
Definition	df-trrels 38564	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 38572. Alternate definitions are dftrrels2 38566 and dftrrels3 38567. This definition is similar to the definitions of the classes of reflexive (df-refrels 38502) and symmetric (df-symrels 38534) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)
⊢ TrRels = ( Trs ∩ Rels )
Definition	df-trrel 38565	Define the transitive relation predicate. (Read: 𝑅 is a transitive relation.) For sets, being an element of the class of transitive relations (df-trrels 38564) is equivalent to satisfying the transitive relation predicate, see eltrrelsrel 38572. Alternate definitions are dftrrel2 38568 and dftrrel3 38569. (Contributed by Peter Mazsa, 17-Jul-2021.)
⊢ ( TrRel 𝑅 ↔ (((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∘ (𝑅 ∩ (dom 𝑅 × ran 𝑅))) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Theorem	dftrrels2 38566	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 5647 (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 38402 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 38567*	Alternate definition of the class of transitive relations. (Contributed by Peter Mazsa, 22-Jul-2021.)
⊢ TrRels = {𝑟 ∈ Rels ∣ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)}
Theorem	dftrrel2 38568	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ Rel 𝑅))
Theorem	dftrrel3 38569*	Alternate definition of the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ ( TrRel 𝑅 ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ Rel 𝑅))
Theorem	eltrrels2 38570	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ 𝑅 ∈ Rels ))
Theorem	eltrrels3 38571*	Element of the class of transitive relations. (Contributed by Peter Mazsa, 22-Aug-2021.)
⊢ (𝑅 ∈ TrRels ↔ (∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ 𝑅 ∈ Rels ))
Theorem	eltrrelsrel 38572	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 38573	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 38574	Any class ' R ' restricted to the singleton of the class ' A ' (see ressn2 38433) is transitive. (Contributed by Peter Mazsa, 17-Jun-2024.)
⊢ TrRel (𝑅 ↾ {𝐴})
21.26.12  Equivalence relations
Definition	df-eqvrels 38575	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 38585. Alternate definitions are dfeqvrels2 38579 and dfeqvrels3 38580. (Contributed by Peter Mazsa, 7-Nov-2018.)
⊢ EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )
Definition	df-eqvrel 38576	Define the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) For sets, being an element of the class of equivalence relations (df-eqvrels 38575) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 38585. Alternate definitions are dfeqvrel2 38581 and dfeqvrel3 38582. (Contributed by Peter Mazsa, 17-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅))
Definition	df-coeleqvrels 38577	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 38587. Alternate definition is dfcoeleqvrels 38612. (Contributed by Peter Mazsa, 28-Nov-2022.)
⊢ CoElEqvRels = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) ∈ EqvRels }
Definition	df-coeleqvrel 38578	Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.) Alternate definition is dfcoeleqvrel 38613. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 38587. (Contributed by Peter Mazsa, 11-Dec-2021.)
⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴))
Theorem	dfeqvrels2 38579	Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.)
⊢ EqvRels = {𝑟 ∈ Rels ∣ (( I ↾ dom 𝑟) ⊆ 𝑟 ∧ ◡𝑟 ⊆ 𝑟 ∧ (𝑟 ∘ 𝑟) ⊆ 𝑟)}
Theorem	dfeqvrels3 38580*	Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019.)
⊢ EqvRels = {𝑟 ∈ Rels ∣ (∀𝑥 ∈ dom 𝑟 𝑥𝑟𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑟𝑦 → 𝑦𝑟𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))}
Theorem	dfeqvrel2 38581	Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ Rel 𝑅))
Theorem	dfeqvrel3 38582*	Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019.)
⊢ ( EqvRel 𝑅 ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ Rel 𝑅))
Theorem	eleqvrels2 38583	Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ EqvRels ↔ ((( I ↾ dom 𝑅) ⊆ 𝑅 ∧ ◡𝑅 ⊆ 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅) ∧ 𝑅 ∈ Rels ))
Theorem	eleqvrels3 38584*	Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021.)
⊢ (𝑅 ∈ EqvRels ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ∧ 𝑅 ∈ Rels ))
Theorem	eleqvrelsrel 38585	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 38586	Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ CoElEqvRels ↔ ≀ (◡ E ↾ 𝐴) ∈ EqvRels ))
Theorem	elcoeleqvrelsrel 38587	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 38588	An equivalence relation is a relation. (Contributed by Peter Mazsa, 2-Jun-2019.)
⊢ ( EqvRel 𝑅 → Rel 𝑅)
Theorem	eqvrelrefrel 38589	An equivalence relation is reflexive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → RefRel 𝑅)
Theorem	eqvrelsymrel 38590	An equivalence relation is symmetric. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → SymRel 𝑅)
Theorem	eqvreltrrel 38591	An equivalence relation is transitive. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → TrRel 𝑅)
Theorem	eqvrelim 38592	Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021.)
⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅)
Theorem	eqvreleq 38593	Equality theorem for equivalence relation. (Contributed by Peter Mazsa, 19-Apr-2020.) (Revised by Peter Mazsa, 23-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvreleqi 38594	Equality theorem for equivalence relation, inference version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ 𝑅 = 𝑆    ⇒   ⊢ ( EqvRel 𝑅 ↔ EqvRel 𝑆)
Theorem	eqvreleqd 38595	Equality theorem for equivalence relation, deduction version. (Contributed by Peter Mazsa, 23-Sep-2021.)
⊢ (𝜑 → 𝑅 = 𝑆)    ⇒   ⊢ (𝜑 → ( EqvRel 𝑅 ↔ EqvRel 𝑆))
Theorem	eqvrelsym 38596	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 38597	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 38598	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 38599	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐵𝑅𝐶)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)
Theorem	eqvreltr4d 38600	A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Peter Mazsa, 2-Jun-2019.)
⊢ (𝜑 → EqvRel 𝑅)    &   ⊢ (𝜑 → 𝐴𝑅𝐵)    &   ⊢ (𝜑 → 𝐶𝑅𝐵)    ⇒   ⊢ (𝜑 → 𝐴𝑅𝐶)