Theorem erthi

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)

	Ref	Expression
Hypotheses	erthi.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
	erthi.2	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
Assertion	erthi	⊢ ( 𝜑 → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		erthi.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2		erthi.2	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
3	1 2	ercl	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
4	1 3	erth	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 ) )
5	2 4	mpbid	⊢ ( 𝜑 → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )