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

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

This definition is similar to the definitions of the classes of symmetric (df-symrels 34776) and transitive (df-trrels 34806) 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 34467 . 2 class RefRels
2 crefs 34466 . . 3 class Refs
3 crels 34464 . . 3 class Rels
42, 3cin 3767 . 2 class ( Refs ∩ Rels )
51, 4wceq 1653 1 wff RefRels = ( Refs ∩ Rels )
Colors of variables: wff setvar class
This definition is referenced by:  dfrefrels2  34750
  Copyright terms: Public domain W3C validator