Definition df-cnvrefrels 38776

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

We use this concept to define functions (df-funsALTV 38936, df-funALTV 38937) and disjoints (df-disjs 38959, df-disjALTV 38960).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38786. Alternate definitions are dfcnvrefrels2 38778 and dfcnvrefrels3 38779. (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 38361	. 2 class CnvRefRels
2		ccnvrefs 38360	. . 3 class CnvRefs
3		crels 38355	. . 3 class Rels
4	2, 3	cin 3899	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1542	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  38778  dfcnvrefrels3  38779