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

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

This definition is similar to the definitions of the classes of symmetric (df-symrels 35897) and transitive (df-trrels 35927) 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 35576 . 2 class RefRels
2 crefs 35575 . . 3 class Refs
3 crels 35573 . . 3 class Rels
42, 3cin 3907 . 2 class ( Refs ∩ Rels )
51, 4wceq 1538 1 wff RefRels = ( Refs ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dfrefrels2  35871
  Copyright terms: Public domain W3C validator