Metamath Proof Explorer

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 ⊢ φ → R Er X
ereldm.2 ⊢ φ → A R = B R
Assertion ereldm ⊢ φ → A ∈ X ↔ B ∈ X

Proof

Step Hyp Ref Expression
1 ereldm.1 ⊢ φ → R Er X
2 ereldm.2 ⊢ φ → A R = B R
3 2 neeq1d ⊢ φ → A R ≠ ∅ ↔ B R ≠ ∅
4 ecdmn0 ⊢ A ∈ dom ⁡ R ↔ A R ≠ ∅
5 ecdmn0 ⊢ B ∈ dom ⁡ R ↔ B R ≠ ∅
6 3 4 5 3bitr4g ⊢ φ → A ∈ dom ⁡ R ↔ B ∈ dom ⁡ R
7 erdm ⊢ R Er X → dom ⁡ R = X
8 1 7 syl ⊢ φ → dom ⁡ R = X
9 8 eleq2d ⊢ φ → A ∈ dom ⁡ R ↔ A ∈ X
10 8 eleq2d ⊢ φ → B ∈ dom ⁡ R ↔ B ∈ X
11 6 9 10 3bitr3d ⊢ φ → A ∈ X ↔ B ∈ X