Metamath Proof Explorer

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 ⊢ φ → dom ⁡ R = A
dmecd.2 ⊢ φ → B R = C R
Assertion dmecd ⊢ φ → B ∈ A ↔ C ∈ A

Proof

Step Hyp Ref Expression
1 dmecd.1 ⊢ φ → dom ⁡ R = A
2 dmecd.2 ⊢ φ → B R = C R
3 2 neeq1d ⊢ φ → B R ≠ ∅ ↔ C R ≠ ∅
4 ecdmn0 ⊢ B ∈ dom ⁡ R ↔ B R ≠ ∅
5 ecdmn0 ⊢ C ∈ dom ⁡ R ↔ C R ≠ ∅
6 3 4 5 3bitr4g ⊢ φ → B ∈ dom ⁡ R ↔ C ∈ dom ⁡ R
7 1 eleq2d ⊢ φ → B ∈ dom ⁡ R ↔ B ∈ A
8 1 eleq2d ⊢ φ → C ∈ dom ⁡ R ↔ C ∈ A
9 6 7 8 3bitr3d ⊢ φ → B ∈ A ↔ C ∈ A