Definition df-eqvrel 38603

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

Assertion

Ref	Expression
df-eqvrel	⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅))

Detailed syntax breakdown of Definition df-eqvrel

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	weqvrel 38216	. 2 wff EqvRel 𝑅
3	1	wrefrel 38205	. . 3 wff RefRel 𝑅
4	1	wsymrel 38211	. . 3 wff SymRel 𝑅
5	1	wtrrel 38214	. . 3 wff TrRel 𝑅
6	3, 4, 5	w3a 1086	. 2 wff ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅)
7	2, 6	wb 206	1 wff ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅))

This definition is referenced by:  dfeqvrel2  38608  dfeqvrel3  38609  eqvrelrefrel  38616  eqvrelsymrel  38617  eqvreltrrel  38618  eqvreleq  38620  eqvrelcoss  38635  refrelredund2  38654