Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cnvrefrels Structured version   Visualization version   GIF version

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

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

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

Assertion
Ref Expression
df-cnvrefrels CnvRefRels = ( CnvRefs ∩ Rels )

Detailed syntax breakdown of Definition df-cnvrefrels
StepHypRef Expression
1 ccnvrefrels 36632 . 2 class CnvRefRels
2 ccnvrefs 36631 . . 3 class CnvRefs
3 crels 36626 . . 3 class Rels
42, 3cin 3909 . 2 class ( CnvRefs ∩ Rels )
51, 4wceq 1541 1 wff CnvRefRels = ( CnvRefs ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dfcnvrefrels2  36980  dfcnvrefrels3  36981
  Copyright terms: Public domain W3C validator