Definition df-cnvrefrels 38617

Description: Define the class of converse reflexive relations. This is practically dfcnvrefrels2 38619 (which uses the traditional subclass relation ⊆) : we use converse subset relation (brcnvssr 38597) here to ensure the comparability to the definitions of the classes of all reflexive (df-ref 23420), symmetric (df-syms 38633) and transitive (df-trs 38667) sets.

We use this concept to define functions (df-funsALTV 38778, df-funALTV 38779) and disjoints (df-disjs 38801, df-disjALTV 38802).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38627. Alternate definitions are dfcnvrefrels2 38619 and dfcnvrefrels3 38620. (Contributed by Peter Mazsa, 7-Jul-2019.)

Assertion

Ref	Expression
df-cnvrefrels	⊢ CnvRefRels = ( CnvRefs ∩ Rels )

Detailed syntax breakdown of Definition df-cnvrefrels

Step	Hyp	Ref	Expression
1		ccnvrefrels 38229	. 2 class CnvRefRels
2		ccnvrefs 38228	. . 3 class CnvRefs
3		crels 38223	. . 3 class Rels
4	2, 3	cin 3896	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1541	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  38619  dfcnvrefrels3  38620