Definition df-cnvrefrels 39729

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

We use this concept to define functions (df-funsALTV 39889, df-funALTV 39890) and disjoints (df-disjs 39912, df-disjALTV 39913).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 39739. Alternate definitions are dfcnvrefrels2 39731 and dfcnvrefrels3 39732. (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 39314	. 2 class CnvRefRels
2		ccnvrefs 39313	. . 3 class CnvRefs
3		crels 39308	. . 3 class Rels
4	2, 3	cin 4092	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1570	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is used by:  dfcnvrefrels2  39731  dfcnvrefrels3  39732