Definition df-cnvrefrels 37935

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

We use this concept to define functions (df-funsALTV 38090, df-funALTV 38091) and disjoints (df-disjs 38113, df-disjALTV 38114).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 37945. Alternate definitions are dfcnvrefrels2 37937 and dfcnvrefrels3 37938. (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 37591	. 2 class CnvRefRels
2		ccnvrefs 37590	. . 3 class CnvRefs
3		crels 37585	. . 3 class Rels
4	2, 3	cin 3943	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1534	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  37937  dfcnvrefrels3  37938