Definition df-cnvrefrels 38523

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

We use this concept to define functions (df-funsALTV 38679, df-funALTV 38680) and disjoints (df-disjs 38702, df-disjALTV 38703).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38533. Alternate definitions are dfcnvrefrels2 38525 and dfcnvrefrels3 38526. (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 38183	. 2 class CnvRefRels
2		ccnvrefs 38182	. . 3 class CnvRefs
3		crels 38177	. . 3 class Rels
4	2, 3	cin 3902	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1540	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  38525  dfcnvrefrels3  38526