Definition df-cnvrefrels 38524

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

We use this concept to define functions (df-funsALTV 38680, df-funALTV 38681) and disjoints (df-disjs 38703, df-disjALTV 38704).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38534. Alternate definitions are dfcnvrefrels2 38526 and dfcnvrefrels3 38527. (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 38184	. 2 class CnvRefRels
2		ccnvrefs 38183	. . 3 class CnvRefs
3		crels 38178	. . 3 class Rels
4	2, 3	cin 3916	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1540	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  38526  dfcnvrefrels3  38527