Metamath Proof Explorer


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 i^i Rels )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnvrefrels
 |-  CnvRefRels
1 ccnvrefs
 |-  CnvRefs
2 crels
 |-  Rels
3 1 2 cin
 |-  ( CnvRefs i^i Rels )
4 0 3 wceq
 |-  CnvRefRels = ( CnvRefs i^i Rels )