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

Definition df-eqvrels 37075
Description: Define the class of equivalence relations. For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 37085. Alternate definitions are dfeqvrels2 37079 and dfeqvrels3 37080. (Contributed by Peter Mazsa, 7-Nov-2018.)
Assertion
Ref Expression
df-eqvrels EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )

Detailed syntax breakdown of Definition df-eqvrels
StepHypRef Expression
1 ceqvrels 36679 . 2 class EqvRels
2 crefrels 36668 . . . 4 class RefRels
3 csymrels 36674 . . . 4 class SymRels
42, 3cin 3914 . . 3 class ( RefRels ∩ SymRels )
5 ctrrels 36677 . . 3 class TrRels
64, 5cin 3914 . 2 class (( RefRels ∩ SymRels ) ∩ TrRels )
71, 6wceq 1542 1 wff EqvRels = (( RefRels ∩ SymRels ) ∩ TrRels )
Colors of variables: wff setvar class
This definition is referenced by:  dfeqvrels2  37079  refrelsredund2  37124
  Copyright terms: Public domain W3C validator