Definition df-cnvrefrels 39110

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

We use this concept to define functions (df-funsALTV 39270, df-funALTV 39271) and disjoints (df-disjs 39293, df-disjALTV 39294).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 39120. Alternate definitions are dfcnvrefrels2 39112 and dfcnvrefrels3 39113. (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 38695	. 2 class CnvRefRels
2		ccnvrefs 38694	. . 3 class CnvRefs
3		crels 38689	. . 3 class Rels
4	2, 3	cin 3905	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1562	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  39112  dfcnvrefrels3  39113