Definition df-cnvrefrels 35924

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

We use this concept to define functions (df-funsALTV 36074, df-funALTV 36075) and disjoints (df-disjs 36097, df-disjALTV 36098).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 35932. Alternate definitions are dfcnvrefrels2 35926 and dfcnvrefrels3 35927. (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 35621	. 2 class CnvRefRels
2		ccnvrefs 35620	. . 3 class CnvRefs
3		crels 35615	. . 3 class Rels
4	2, 3	cin 3880	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1538	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  35926  dfcnvrefrels3  35927