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 ) )