This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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