This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-eqvrel

Description: Define the equivalence relation predicate. (Read: R is an equivalence relation.) For sets, being an element of the class of equivalence relations ( df-eqvrels ) is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel . Alternate definitions are dfeqvrel2 and dfeqvrel3 . (Contributed by Peter Mazsa, 17-Apr-2019)

Ref Expression
Assertion df-eqvrel 
|- ( EqvRel R <-> ( RefRel R /\ SymRel R /\ TrRel R ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 0 weqvrel 
 |-  EqvRel R
2 0 wrefrel 
 |-  RefRel R
3 0 wsymrel 
 |-  SymRel R
4 0 wtrrel 
 |-  TrRel R
5 2 3 4 w3a 
 |-  ( RefRel R /\ SymRel R /\ TrRel R )
6 1 5 wb 
 |-  ( EqvRel R <-> ( RefRel R /\ SymRel R /\ TrRel R ) )