This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-eqvrels

Description: Define the class of equivalence relations. For sets, being an element of the class of equivalence relations is equivalent to satisfying the equivalence relation predicate, see eleqvrelsrel . Alternate definitions are dfeqvrels2 and dfeqvrels3 . (Contributed by Peter Mazsa, 7-Nov-2018)

		Ref	Expression
	Assertion	df-eqvrels	⊢ EqvRels = ( ( RefRels ∩ SymRels ) ∩ TrRels )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceqvrels	⊢ EqvRels
1		crefrels	⊢ RefRels
2		csymrels	⊢ SymRels
3	1 2	cin	⊢ ( RefRels ∩ SymRels )
4		ctrrels	⊢ TrRels
5	3 4	cin	⊢ ( ( RefRels ∩ SymRels ) ∩ TrRels )
6	0 5	wceq	⊢ EqvRels = ( ( RefRels ∩ SymRels ) ∩ TrRels )