Step | Hyp | Ref
| Expression |
1 | | eleq1d.1 |
. . . 4
⊢ (𝜑 → 𝐴 = 𝐵) |
2 | | dfcleq 2731 |
. . . 4
⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | 1, 2 | sylib 221 |
. . 3
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
4 | | anbi2 636 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
5 | 4 | alexbii 1840 |
. . 3
⊢
(∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
6 | 3, 5 | syl 17 |
. 2
⊢ (𝜑 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))) |
7 | | dfclel 2818 |
. 2
⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴)) |
8 | | dfclel 2818 |
. 2
⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)) |
9 | 6, 7, 8 | 3bitr4g 317 |
1
⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) |