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

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

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