Definition df-cnvrefrels 38988

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

We use this concept to define functions (df-funsALTV 39148, df-funALTV 39149) and disjoints (df-disjs 39171, df-disjALTV 39172).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38998. Alternate definitions are dfcnvrefrels2 38990 and dfcnvrefrels3 38991. (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 38573	. 2 class CnvRefRels
2		ccnvrefs 38572	. . 3 class CnvRefs
3		crels 38567	. . 3 class Rels
4	2, 3	cin 3884	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1548	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  38990  dfcnvrefrels3  38991