Step | Hyp | Ref
| Expression |
1 | | 2sb6 2090 |
. . . . . . . . 9
⊢ ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ ∀𝑧∀𝑥((𝑧 = 𝑣 ∧ 𝑥 = 𝑢) → 𝜑)) |
2 | | alcom 2159 |
. . . . . . . . 9
⊢
(∀𝑧∀𝑥((𝑧 = 𝑣 ∧ 𝑥 = 𝑢) → 𝜑) ↔ ∀𝑥∀𝑧((𝑧 = 𝑣 ∧ 𝑥 = 𝑢) → 𝜑)) |
3 | | ancomst 467 |
. . . . . . . . . 10
⊢ (((𝑧 = 𝑣 ∧ 𝑥 = 𝑢) → 𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑧 = 𝑣) → 𝜑)) |
4 | 3 | 2albii 1817 |
. . . . . . . . 9
⊢
(∀𝑥∀𝑧((𝑧 = 𝑣 ∧ 𝑥 = 𝑢) → 𝜑) ↔ ∀𝑥∀𝑧((𝑥 = 𝑢 ∧ 𝑧 = 𝑣) → 𝜑)) |
5 | 1, 2, 4 | 3bitri 299 |
. . . . . . . 8
⊢ ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ ∀𝑥∀𝑧((𝑥 = 𝑢 ∧ 𝑧 = 𝑣) → 𝜑)) |
6 | | 2sb6 2090 |
. . . . . . . 8
⊢ ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ ∀𝑥∀𝑧((𝑥 = 𝑢 ∧ 𝑧 = 𝑣) → 𝜑)) |
7 | 5, 6 | bitr4i 280 |
. . . . . . 7
⊢ ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ [𝑢 / 𝑥][𝑣 / 𝑧]𝜑) |
8 | | sbequ 2086 |
. . . . . . . 8
⊢ (𝑢 = 𝑦 → ([𝑢 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
9 | 8 | sbbidv 2080 |
. . . . . . 7
⊢ (𝑢 = 𝑦 → ([𝑣 / 𝑧][𝑢 / 𝑥]𝜑 ↔ [𝑣 / 𝑧][𝑦 / 𝑥]𝜑)) |
10 | 7, 9 | syl5bbr 287 |
. . . . . 6
⊢ (𝑢 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑣 / 𝑧][𝑦 / 𝑥]𝜑)) |
11 | | sbequ 2086 |
. . . . . 6
⊢ (𝑣 = 𝑤 → ([𝑣 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜑)) |
12 | 10, 11 | sylan9bb 512 |
. . . . 5
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑤 / 𝑧][𝑦 / 𝑥]𝜑)) |
13 | | sbequ 2086 |
. . . . . . 7
⊢ (𝑣 = 𝑤 → ([𝑣 / 𝑧]𝜑 ↔ [𝑤 / 𝑧]𝜑)) |
14 | 13 | sbbidv 2080 |
. . . . . 6
⊢ (𝑣 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑢 / 𝑥][𝑤 / 𝑧]𝜑)) |
15 | | sbequ 2086 |
. . . . . 6
⊢ (𝑢 = 𝑦 → ([𝑢 / 𝑥][𝑤 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)) |
16 | 14, 15 | sylan9bbr 513 |
. . . . 5
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)) |
17 | 12, 16 | bitr3d 283 |
. . . 4
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)) |
18 | 17 | ex 415 |
. . 3
⊢ (𝑢 = 𝑦 → (𝑣 = 𝑤 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))) |
19 | | ax6ev 1968 |
. . 3
⊢
∃𝑢 𝑢 = 𝑦 |
20 | 18, 19 | exlimiiv 1928 |
. 2
⊢ (𝑣 = 𝑤 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)) |
21 | | ax6ev 1968 |
. 2
⊢
∃𝑣 𝑣 = 𝑤 |
22 | 20, 21 | exlimiiv 1928 |
1
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑) |