Definition df-cnvrefrels 39341

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

We use this concept to define functions (df-funsALTV 39501, df-funALTV 39502) and disjoints (df-disjs 39524, df-disjALTV 39525).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 39351. Alternate definitions are dfcnvrefrels2 39343 and dfcnvrefrels3 39344. (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 38926	. 2 class CnvRefRels
2		ccnvrefs 38925	. . 3 class CnvRefs
3		crels 38920	. . 3 class Rels
4	2, 3	cin 3901	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1570	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is used by:  dfcnvrefrels2  39343  dfcnvrefrels3  39344