Definition df-cnvrefrels 38947

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

We use this concept to define functions (df-funsALTV 39107, df-funALTV 39108) and disjoints (df-disjs 39130, df-disjALTV 39131).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38957. Alternate definitions are dfcnvrefrels2 38949 and dfcnvrefrels3 38950. (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 38532	. 2 class CnvRefRels
2		ccnvrefs 38531	. . 3 class CnvRefs
3		crels 38526	. . 3 class Rels
4	2, 3	cin 3889	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1542	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  38949  dfcnvrefrels3  38950