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

Metamath Proof Explorer

Theorem eqvrelthi

Description: Basic property of equivalence relations. Part of Lemma 3N of Enderton p. 57. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 9-Jul-2014) (Revised by Peter Mazsa, 2-Jun-2019)

	Ref	Expression
Hypotheses	eqvrelthi.1	$⊢ φ \to EqvRel R$
	eqvrelthi.2	$⊢ φ \to A R B$
Assertion	eqvrelthi	$⊢ φ \to [A] R = [B] R$

Proof

Step	Hyp	Ref	Expression
1		eqvrelthi.1	$⊢ φ \to EqvRel R$
2		eqvrelthi.2	$⊢ φ \to A R B$
3	1 2	eqvrelcl	$⊢ φ \to A \in dom R$
4	1 3	eqvrelth	$⊢ φ \to (A R B \leftrightarrow [A] R = [B] R)$
5	2 4	mpbid	$⊢ φ \to [A] R = [B] R$