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

Definition df-eqvrel 37038
Description: Define the equivalence relation predicate. (Read: 𝑅 is an equivalence relation.) For sets, being an element of the class of equivalence relations (df-eqvrels 37037) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel 37047. Alternate definitions are dfeqvrel2 37043 and dfeqvrel3 37044. (Contributed by Peter Mazsa, 17-Apr-2019.)
Assertion
Ref Expression
df-eqvrel ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅))

Detailed syntax breakdown of Definition df-eqvrel
StepHypRef Expression
1 cR . . 3 class 𝑅
21weqvrel 36642 . 2 wff EqvRel 𝑅
31wrefrel 36631 . . 3 wff RefRel 𝑅
41wsymrel 36637 . . 3 wff SymRel 𝑅
51wtrrel 36640 . . 3 wff TrRel 𝑅
63, 4, 5w3a 1087 . 2 wff ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅)
72, 6wb 205 1 wff ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅))
Colors of variables: wff setvar class
This definition is referenced by:  dfeqvrel2  37043  dfeqvrel3  37044  eqvrelrefrel  37051  eqvrelsymrel  37052  eqvreltrrel  37053  eqvreleq  37055  eqvrelcoss  37070  refrelredund2  37089
  Copyright terms: Public domain W3C validator