Definition df-cnvrefrels 38482

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

We use this concept to define functions (df-funsALTV 38637, df-funALTV 38638) and disjoints (df-disjs 38660, df-disjALTV 38661).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38492. Alternate definitions are dfcnvrefrels2 38484 and dfcnvrefrels3 38485. (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 38143	. 2 class CnvRefRels
2		ccnvrefs 38142	. . 3 class CnvRefs
3		crels 38137	. . 3 class Rels
4	2, 3	cin 3975	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1537	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  38484  dfcnvrefrels3  38485