Metamath Proof Explorer

Theorem erth2

Description: Basic property of equivalence relations. Compare Theorem 73 of Suppes p. 82. Assumes membership of the second argument in the domain. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 6-Jul-2015)

	Ref	Expression
Hypotheses	erth2.1	$⊢ φ \to R Er X$
	erth2.2	$⊢ φ \to B \in X$
Assertion	erth2	$⊢ φ \to (A R B \leftrightarrow [A] R = [B] R)$

Proof

Step	Hyp	Ref	Expression
1		erth2.1	$⊢ φ \to R Er X$
2		erth2.2	$⊢ φ \to B \in X$
3	1	ersymb	$⊢ φ \to (A R B \leftrightarrow B R A)$
4	1 2	erth	$⊢ φ \to (B R A \leftrightarrow [B] R = [A] R)$
5		eqcom	$⊢ [B] R = [A] R \leftrightarrow [A] R = [B] R$
6	4 5	syl6bb	$⊢ φ \to (B R A \leftrightarrow [A] R = [B] R)$
7	3 6	bitrd	$⊢ φ \to (A R B \leftrightarrow [A] R = [B] R)$