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 𝑅 = 𝐴 ) | |
| dmecd.2 | ⊢ ( 𝜑 → [ 𝐵 ] 𝑅 = [ 𝐶 ] 𝑅 ) | ||
| Assertion | dmecd | ⊢ ( 𝜑 → ( 𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmecd.1 | ⊢ ( 𝜑 → dom 𝑅 = 𝐴 ) | |
| 2 | dmecd.2 | ⊢ ( 𝜑 → [ 𝐵 ] 𝑅 = [ 𝐶 ] 𝑅 ) | |
| 3 | 2 | neeq1d | ⊢ ( 𝜑 → ( [ 𝐵 ] 𝑅 ≠ ∅ ↔ [ 𝐶 ] 𝑅 ≠ ∅ ) ) |
| 4 | ecdmn0 | ⊢ ( 𝐵 ∈ dom 𝑅 ↔ [ 𝐵 ] 𝑅 ≠ ∅ ) | |
| 5 | ecdmn0 | ⊢ ( 𝐶 ∈ dom 𝑅 ↔ [ 𝐶 ] 𝑅 ≠ ∅ ) | |
| 6 | 3 4 5 | 3bitr4g | ⊢ ( 𝜑 → ( 𝐵 ∈ dom 𝑅 ↔ 𝐶 ∈ dom 𝑅 ) ) |
| 7 | 1 | eleq2d | ⊢ ( 𝜑 → ( 𝐵 ∈ dom 𝑅 ↔ 𝐵 ∈ 𝐴 ) ) |
| 8 | 1 | eleq2d | ⊢ ( 𝜑 → ( 𝐶 ∈ dom 𝑅 ↔ 𝐶 ∈ 𝐴 ) ) |
| 9 | 6 7 8 | 3bitr3d | ⊢ ( 𝜑 → ( 𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) ) |