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 38050
Description: Define the class of converse reflexive relations. This is practically dfcnvrefrels2 38052 (which uses the traditional subclass relation ) : we use converse subset relation (brcnvssr 38030) here to ensure the comparability to the definitions of the classes of all reflexive (df-ref 23422), symmetric (df-syms 38066) and transitive (df-trs 38096) sets.

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

For sets, being an element of the class of converse reflexive relations is equivalent to satisfying the converse reflexive relation predicate, see elcnvrefrelsrel 38060. Alternate definitions are dfcnvrefrels2 38052 and dfcnvrefrels3 38053. (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 37709 . 2 class CnvRefRels
2 ccnvrefs 37708 . . 3 class CnvRefs
3 crels 37703 . . 3 class Rels
42, 3cin 3940 . 2 class ( CnvRefs ∩ Rels )
51, 4wceq 1533 1 wff CnvRefRels = ( CnvRefs ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dfcnvrefrels2  38052  dfcnvrefrels3  38053
  Copyright terms: Public domain W3C validator