Definition df-cnvrefrels 35779

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

We use this concept to define functions (df-funsALTV 35929, df-funALTV 35930) and disjoints (df-disjs 35952, df-disjALTV 35953).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 35787. Alternate definitions are dfcnvrefrels2 35781 and dfcnvrefrels3 35782. (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 35476	. 2 class CnvRefRels
2		ccnvrefs 35475	. . 3 class CnvRefs
3		crels 35470	. . 3 class Rels
4	2, 3	cin 3935	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1537	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  35781  dfcnvrefrels3  35782