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 37467
Description: Define the class of reflexive relations. This is practically dfrefrels2 37469 (which reveals that RefRels can not include proper classes like I as is elements, see comments of dfrefrels2 37469).

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

This definition is similar to the definitions of the classes of symmetric (df-symrels 37499) and transitive (df-trrels 37529) 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 37134 . 2 class RefRels
2 crefs 37133 . . 3 class Refs
3 crels 37131 . . 3 class Rels
42, 3cin 3947 . 2 class ( Refs ∩ Rels )
51, 4wceq 1541 1 wff RefRels = ( Refs ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dfrefrels2  37469
  Copyright terms: Public domain W3C validator