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	|- ( ph -> [ B ] R = [ C ] R )
Assertion	dmec2d	|- ( ph -> ( B e. dom R <-> C e. dom R ) )

Proof

Step	Hyp	Ref	Expression
1		dmec2d.1	|- ( ph -> [ B ] R = [ C ] R )
2		eqidd	|- ( ph -> dom R = dom R )
3	2 1	dmecd	|- ( ph -> ( B e. dom R <-> C e. dom R ) )