Theorem dmecd

Description: Equality of the coset of B and the coset of C implies equivalence of domain elementhood (equivalence is not necessary as opposed to ereldm ). (Contributed by Peter Mazsa, 9-Oct-2018)

	Ref	Expression
Hypotheses	dmecd.1	$$⊢\phi \to \mathrm{dom}R=A$$
	dmecd.2	$$⊢\phi \to \left[B\right]R=\left[C\right]R$$
Assertion	dmecd	$$⊢\phi \to \left(B\in A\leftrightarrow C\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dmecd.1	$$⊢\phi \to \mathrm{dom}R=A$$
2		dmecd.2	$$⊢\phi \to \left[B\right]R=\left[C\right]R$$
3	2	neeq1d	$$⊢\phi \to \left(\left[B\right]R\ne \varnothing \leftrightarrow \left[C\right]R\ne \varnothing \right)$$
4		ecdmn0	$$⊢B\in \mathrm{dom}R\leftrightarrow \left[B\right]R\ne \varnothing$$
5		ecdmn0	$$⊢C\in \mathrm{dom}R\leftrightarrow \left[C\right]R\ne \varnothing$$
6	3 4 5	3bitr4g	$$⊢\phi \to \left(B\in \mathrm{dom}R\leftrightarrow C\in \mathrm{dom}R\right)$$
7	1	eleq2d	$$⊢\phi \to \left(B\in \mathrm{dom}R\leftrightarrow B\in A\right)$$
8	1	eleq2d	$$⊢\phi \to \left(C\in \mathrm{dom}R\leftrightarrow C\in A\right)$$
9	6 7 8	3bitr3d	$$⊢\phi \to \left(B\in A\leftrightarrow C\in A\right)$$