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

Definition df-refrels 34603
Description: Define the class of all reflexive relations. This is practically dfrefrels2 34605 (which reveals that RefRels can not include proper classes like I as is elements, cf. the comments of dfrefrels2 34605).

Another alternative definition is dfrefrels3 34606. The element of this class and the reflexive relation predicate (df-refrel 34604) are the same, that is, (𝑅 ∈ RefRels ↔ RefRel 𝑅) when 𝐴 is a set, cf. elrefrelsrel 34611.

This definition is similar to the definitions of the classes of all symmetric (df-symrels 34631) and transitive ( ~? df-trrels ) relations. (Contributed by Peter Mazsa, 7-Jul-2019.)

Assertion
Ref Expression
df-refrels RefRels = ( Refs ∩ Rels )

Detailed syntax breakdown of Definition df-refrels
StepHypRef Expression
1 crefrels 34320 . 2 class RefRels
2 crefs 34319 . . 3 class Refs
3 crels 34317 . . 3 class Rels
42, 3cin 3722 . 2 class ( Refs ∩ Rels )
51, 4wceq 1631 1 wff RefRels = ( Refs ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dfrefrels2  34605
  Copyright terms: Public domain W3C validator