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\leftrightarrow 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 \leftrightarrow \left[B\right]R\ne \varnothing \right)$$
4		ecdmn0	$$⊢A\in \mathrm{dom}R\leftrightarrow \left[A\right]R\ne \varnothing$$
5		ecdmn0	$$⊢B\in \mathrm{dom}R\leftrightarrow \left[B\right]R\ne \varnothing$$
6	3 4 5	3bitr4g	$$⊢\phi \to \left(A\in \mathrm{dom}R\leftrightarrow 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\leftrightarrow A\in X\right)$$
10	8	eleq2d	$$⊢\phi \to \left(B\in \mathrm{dom}R\leftrightarrow B\in X\right)$$
11	6 9 10	3bitr3d	$$⊢\phi \to \left(A\in X\leftrightarrow B\in X\right)$$