Definition df-cnvrefrels 39283

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

We use this concept to define functions (df-funsALTV 39443, df-funALTV 39444) and disjoints (df-disjs 39466, df-disjALTV 39467).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 39293. Alternate definitions are dfcnvrefrels2 39285 and dfcnvrefrels3 39286. (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 38868	. 2 class CnvRefRels
2		ccnvrefs 38867	. . 3 class CnvRefs
3		crels 38862	. . 3 class Rels
4	2, 3	cin 3903	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1569	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is used by:  dfcnvrefrels2  39285  dfcnvrefrels3  39286