Definition df-cnvrefrels 39295

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

We use this concept to define functions (df-funsALTV 39455, df-funALTV 39456) and disjoints (df-disjs 39478, df-disjALTV 39479).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 39305. Alternate definitions are dfcnvrefrels2 39297 and dfcnvrefrels3 39298. (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 38880	. 2 class CnvRefRels
2		ccnvrefs 38879	. . 3 class CnvRefs
3		crels 38874	. . 3 class Rels
4	2, 3	cin 3907	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1570	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is used by:  dfcnvrefrels2  39297  dfcnvrefrels3  39298