Definition df-cnvrefrels 38507

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

We use this concept to define functions (df-funsALTV 38662, df-funALTV 38663) and disjoints (df-disjs 38685, df-disjALTV 38686).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38517. Alternate definitions are dfcnvrefrels2 38509 and dfcnvrefrels3 38510. (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 38169	. 2 class CnvRefRels
2		ccnvrefs 38168	. . 3 class CnvRefs
3		crels 38163	. . 3 class Rels
4	2, 3	cin 3961	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1536	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  38509  dfcnvrefrels3  38510