Definition df-cnvrefrels 36621

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

We use this concept to define functions (df-funsALTV 36771, df-funALTV 36772) and disjoints (df-disjs 36794, df-disjALTV 36795).

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 36629. Alternate definitions are dfcnvrefrels2 36623 and dfcnvrefrels3 36624. (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 36320	. 2 class CnvRefRels
2		ccnvrefs 36319	. . 3 class CnvRefs
3		crels 36314	. . 3 class Rels
4	2, 3	cin 3890	. 2 class ( CnvRefs ∩ Rels )
5	1, 4	wceq 1541	1 wff CnvRefRels = ( CnvRefs ∩ Rels )

This definition is referenced by:  dfcnvrefrels2  36623  dfcnvrefrels3  36624