# 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 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
ereldm.2 ${⊢}{\phi }\to \left[{A}\right]{R}=\left[{B}\right]{R}$
Assertion ereldm ${⊢}{\phi }\to \left({A}\in {X}↔{B}\in {X}\right)$

### Proof

Step Hyp Ref Expression
1 ereldm.1 ${⊢}{\phi }\to {R}\mathrm{Er}{X}$
2 ereldm.2 ${⊢}{\phi }\to \left[{A}\right]{R}=\left[{B}\right]{R}$
3 2 neeq1d ${⊢}{\phi }\to \left(\left[{A}\right]{R}\ne \varnothing ↔\left[{B}\right]{R}\ne \varnothing \right)$
4 ecdmn0 ${⊢}{A}\in \mathrm{dom}{R}↔\left[{A}\right]{R}\ne \varnothing$
5 ecdmn0 ${⊢}{B}\in \mathrm{dom}{R}↔\left[{B}\right]{R}\ne \varnothing$
6 3 4 5 3bitr4g ${⊢}{\phi }\to \left({A}\in \mathrm{dom}{R}↔{B}\in \mathrm{dom}{R}\right)$
7 erdm ${⊢}{R}\mathrm{Er}{X}\to \mathrm{dom}{R}={X}$
8 1 7 syl ${⊢}{\phi }\to \mathrm{dom}{R}={X}$
9 8 eleq2d ${⊢}{\phi }\to \left({A}\in \mathrm{dom}{R}↔{A}\in {X}\right)$
10 8 eleq2d ${⊢}{\phi }\to \left({B}\in \mathrm{dom}{R}↔{B}\in {X}\right)$
11 6 9 10 3bitr3d ${⊢}{\phi }\to \left({A}\in {X}↔{B}\in {X}\right)$