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	⊢ CnvRefRels = ( CnvRefs ∩ Rels )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnvrefrels	⊢ CnvRefRels
1		ccnvrefs	⊢ CnvRefs
2		crels	⊢ Rels
3	1 2	cin	⊢ ( CnvRefs ∩ Rels )
4	0 3	wceq	⊢ CnvRefRels = ( CnvRefs ∩ Rels )