Definition df-cnvrefrels 37391

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

We use this concept to define functions (df-funsALTV 37546, df-funALTV 37547) and disjoints (df-disjs 37569, df-disjALTV 37570).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 37401. Alternate definitions are dfcnvrefrels2 37393 and dfcnvrefrels3 37394. (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 37046	. 2 class CnvRefRels
2		ccnvrefs 37045	. . 3 class CnvRefs
3		crels 37040	. . 3 class Rels
4	2, 3	cin 3947	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1541	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  37393  dfcnvrefrels3  37394