Definition df-cnvrefrels 39539

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

We use this concept to define functions (df-funsALTV 39699, df-funALTV 39700) and disjoints (df-disjs 39722, df-disjALTV 39723).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 39549. Alternate definitions are dfcnvrefrels2 39541 and dfcnvrefrels3 39542. (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 39124	. 2 class CnvRefRels
2		ccnvrefs 39123	. . 3 class CnvRefs
3		crels 39118	. . 3 class Rels
4	2, 3	cin 4089	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1569	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is used by:  dfcnvrefrels2  39541  dfcnvrefrels3  39542