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 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	weqvrel	⊢ EqvRel 𝑅
2	0	wrefrel	⊢ RefRel 𝑅
3	0	wsymrel	⊢ SymRel 𝑅
4	0	wtrrel	⊢ TrRel 𝑅
5	2 3 4	w3a	⊢ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 )
6	1 5	wb	⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) )