Metamath Proof Explorer

Theorem dmec2d

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, 12-Oct-2018)

		Ref	Expression
	Hypothesis	dmec2d.1	$⊢ φ \to [B] R = [C] R$
	Assertion	dmec2d	$⊢ φ \to (B \in dom R \leftrightarrow C \in dom R)$

Proof

Step	Hyp	Ref	Expression
1		dmec2d.1	$⊢ φ \to [B] R = [C] R$
2		eqidd	$⊢ φ \to dom R = dom R$
3	2 1	dmecd	$⊢ φ \to (B \in dom R \leftrightarrow C \in dom R)$