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	$$⊢EqvRelR\leftrightarrow \left(RefRelR\wedge SymRelR\wedge TrRelR\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1	0	weqvrel	$$wffEqvRelR$$
2	0	wrefrel	$$wffRefRelR$$
3	0	wsymrel	$$wffSymRelR$$
4	0	wtrrel	$$wffTrRelR$$
5	2 3 4	w3a	$$wff\left(RefRelR\wedge SymRelR\wedge TrRelR\right)$$
6	1 5	wb	$$wff\left(EqvRelR\leftrightarrow \left(RefRelR\wedge SymRelR\wedge TrRelR\right)\right)$$