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 class R
1 0 weqvrel wff EqvRel R
2 0 wrefrel wff RefRel R
3 0 wsymrel wff SymRel R
4 0 wtrrel wff TrRel R
5 2 3 4 w3a wff RefRel R SymRel R TrRel R
6 1 5 wb wff EqvRel R RefRel R SymRel R TrRel R