Definition df-cnvrefrels

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

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

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel . Alternate definitions are dfcnvrefrels2 and dfcnvrefrels3 . (Contributed by Peter Mazsa, 7-Jul-2019)

	Ref	Expression
Assertion	df-cnvrefrels	$$⊢\mathrm{CnvRefRels}=\mathrm{CnvRefs}\cap \mathrm{Rels}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnvrefrels	$$class\mathrm{CnvRefRels}$$
1		ccnvrefs	$$class\mathrm{CnvRefs}$$
2		crels	$$class\mathrm{Rels}$$
3	1 2	cin	$$class\left(\mathrm{CnvRefs}\cap \mathrm{Rels}\right)$$
4	0 3	wceq	$$wff\mathrm{CnvRefRels}=\mathrm{CnvRefs}\cap \mathrm{Rels}$$