Step | Hyp | Ref
| Expression |
1 | | eqeq2 2750 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑤 = 𝑦 ↔ 𝑤 = 𝐵)) |
2 | 1 | anbi2d 632 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ↔ (𝑧 = 𝑥 ∧ 𝑤 = 𝐵))) |
3 | 2 | anbi1d 633 |
. . . . 5
⊢ (𝑦 = 𝐵 → (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ ((𝑧 = 𝑥 ∧ 𝑤 = 𝐵) ∧ 𝜑))) |
4 | 3 | 2exbidv 1931 |
. . . 4
⊢ (𝑦 = 𝐵 → (∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝐵) ∧ 𝜑))) |
5 | | dfsbcq 3682 |
. . . . 5
⊢ (𝑦 = 𝐵 → ([𝑦 / 𝑤]𝜑 ↔ [𝐵 / 𝑤]𝜑)) |
6 | 5 | sbcbidv 3736 |
. . . 4
⊢ (𝑦 = 𝐵 → ([𝑥 / 𝑧][𝑦 / 𝑤]𝜑 ↔ [𝑥 / 𝑧][𝐵 / 𝑤]𝜑)) |
7 | 4, 6 | bibi12d 349 |
. . 3
⊢ (𝑦 = 𝐵 → ((∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ [𝑥 / 𝑧][𝑦 / 𝑤]𝜑) ↔ (∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝑥 / 𝑧][𝐵 / 𝑤]𝜑))) |
8 | | eqeq2 2750 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑧 = 𝑥 ↔ 𝑧 = 𝐴)) |
9 | 8 | anbi1d 633 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑧 = 𝑥 ∧ 𝑤 = 𝐵) ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵))) |
10 | 9 | anbi1d 633 |
. . . . 5
⊢ (𝑥 = 𝐴 → (((𝑧 = 𝑥 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ ((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑))) |
11 | 10 | 2exbidv 1931 |
. . . 4
⊢ (𝑥 = 𝐴 → (∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ ∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑))) |
12 | | dfsbcq 3682 |
. . . 4
⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑧][𝐵 / 𝑤]𝜑 ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)) |
13 | 11, 12 | bibi12d 349 |
. . 3
⊢ (𝑥 = 𝐴 → ((∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝑥 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))) |
14 | | sbc5 3708 |
. . . 4
⊢
([𝑥 / 𝑧][𝑦 / 𝑤]𝜑 ↔ ∃𝑧(𝑧 = 𝑥 ∧ [𝑦 / 𝑤]𝜑)) |
15 | | 19.42v 1961 |
. . . . . 6
⊢
(∃𝑤(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑)) ↔ (𝑧 = 𝑥 ∧ ∃𝑤(𝑤 = 𝑦 ∧ 𝜑))) |
16 | | anass 472 |
. . . . . . 7
⊢ (((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ (𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑))) |
17 | 16 | exbii 1854 |
. . . . . 6
⊢
(∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ ∃𝑤(𝑧 = 𝑥 ∧ (𝑤 = 𝑦 ∧ 𝜑))) |
18 | | sbc5 3708 |
. . . . . . 7
⊢
([𝑦 / 𝑤]𝜑 ↔ ∃𝑤(𝑤 = 𝑦 ∧ 𝜑)) |
19 | 18 | anbi2i 626 |
. . . . . 6
⊢ ((𝑧 = 𝑥 ∧ [𝑦 / 𝑤]𝜑) ↔ (𝑧 = 𝑥 ∧ ∃𝑤(𝑤 = 𝑦 ∧ 𝜑))) |
20 | 15, 17, 19 | 3bitr4ri 307 |
. . . . 5
⊢ ((𝑧 = 𝑥 ∧ [𝑦 / 𝑤]𝜑) ↔ ∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑)) |
21 | 20 | exbii 1854 |
. . . 4
⊢
(∃𝑧(𝑧 = 𝑥 ∧ [𝑦 / 𝑤]𝜑) ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑)) |
22 | 14, 21 | bitr2i 279 |
. . 3
⊢
(∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ 𝜑) ↔ [𝑥 / 𝑧][𝑦 / 𝑤]𝜑) |
23 | 7, 13, 22 | vtocl2g 3475 |
. 2
⊢ ((𝐵 ∈ 𝐷 ∧ 𝐴 ∈ 𝐶) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)) |
24 | 23 | ancoms 462 |
1
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)) |