Definition df-cnvrefrels 35238

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

We use this concept to define functions (df-funsALTV 35388, df-funALTV 35389) and disjoints (df-disjs 35411, df-disjALTV 35412).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 35246. Alternate definitions are dfcnvrefrels2 35240 and dfcnvrefrels3 35241. (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 34934	. 2 class CnvRefRels
2		ccnvrefs 34933	. . 3 class CnvRefs
3		crels 34928	. . 3 class Rels
4	2, 3	cin 3822	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1507	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  35240  dfcnvrefrels3  35241