Theorem ereldm

Description: Equality of equivalence classes implies equivalence of domain membership. (Contributed by NM, 28-Jan-1996) (Revised by Mario Carneiro, 12-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ereldm.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2		ereldm.2	⊢ ( 𝜑 → [ 𝐴 ] 𝑅 = [ 𝐵 ] 𝑅 )
3	2	neeq1d	⊢ ( 𝜑 → ( [ 𝐴 ] 𝑅 ≠ ∅ ↔ [ 𝐵 ] 𝑅 ≠ ∅ ) )
4		ecdmn0	⊢ ( 𝐴 ∈ dom 𝑅 ↔ [ 𝐴 ] 𝑅 ≠ ∅ )
5		ecdmn0	⊢ ( 𝐵 ∈ dom 𝑅 ↔ [ 𝐵 ] 𝑅 ≠ ∅ )
6	3 4 5	3bitr4g	⊢ ( 𝜑 → ( 𝐴 ∈ dom 𝑅 ↔ 𝐵 ∈ dom 𝑅 ) )
7		erdm	⊢ ( 𝑅 Er 𝑋 → dom 𝑅 = 𝑋 )
8	1 7	syl	⊢ ( 𝜑 → dom 𝑅 = 𝑋 )
9	8	eleq2d	⊢ ( 𝜑 → ( 𝐴 ∈ dom 𝑅 ↔ 𝐴 ∈ 𝑋 ) )
10	8	eleq2d	⊢ ( 𝜑 → ( 𝐵 ∈ dom 𝑅 ↔ 𝐵 ∈ 𝑋 ) )
11	6 9 10	3bitr3d	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋 ) )