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	⊢ ( 𝜑 → [ 𝐵 ] 𝑅 = [ 𝐶 ] 𝑅 )
Assertion	dmec2d	⊢ ( 𝜑 → ( 𝐵 ∈ dom 𝑅 ↔ 𝐶 ∈ dom 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		dmec2d.1	⊢ ( 𝜑 → [ 𝐵 ] 𝑅 = [ 𝐶 ] 𝑅 )
2		eqidd	⊢ ( 𝜑 → dom 𝑅 = dom 𝑅 )
3	2 1	dmecd	⊢ ( 𝜑 → ( 𝐵 ∈ dom 𝑅 ↔ 𝐶 ∈ dom 𝑅 ) )