Proof of Theorem spc3gv
Step | Hyp | Ref
| Expression |
1 | | elisset 2562 |
. . . 4
⊢ (A ∈ 𝑉 → ∃x x = A) |
2 | | elisset 2562 |
. . . 4
⊢ (B ∈ 𝑊 → ∃y y = B) |
3 | | elisset 2562 |
. . . 4
⊢ (𝐶 ∈ 𝑋 → ∃z z = 𝐶) |
4 | 1, 2, 3 | 3anim123i 1088 |
. . 3
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃x x = A ∧ ∃y y = B ∧ ∃z z = 𝐶)) |
5 | | eeeanv 1805 |
. . 3
⊢ (∃x∃y∃z(x = A ∧ y = B ∧ z = 𝐶) ↔ (∃x x = A ∧ ∃y y = B ∧ ∃z z = 𝐶)) |
6 | 4, 5 | sylibr 137 |
. 2
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ∃x∃y∃z(x = A ∧ y = B ∧ z = 𝐶)) |
7 | | spc3egv.1 |
. . . . . . . 8
⊢
((x = A ∧ y = B ∧ z = 𝐶) → (φ ↔ ψ)) |
8 | 7 | biimpcd 148 |
. . . . . . 7
⊢ (φ → ((x = A ∧ y = B ∧ z = 𝐶) → ψ)) |
9 | 8 | 2alimi 1342 |
. . . . . 6
⊢ (∀y∀zφ → ∀y∀z((x = A ∧ y = B ∧ z = 𝐶) → ψ)) |
10 | 9 | alimi 1341 |
. . . . 5
⊢ (∀x∀y∀zφ → ∀x∀y∀z((x = A ∧ y = B ∧ z = 𝐶) → ψ)) |
11 | | exim 1487 |
. . . . . 6
⊢ (∀z((x = A ∧ y = B ∧ z = 𝐶) → ψ) → (∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃zψ)) |
12 | 11 | 2alimi 1342 |
. . . . 5
⊢ (∀x∀y∀z((x = A ∧ y = B ∧ z = 𝐶) → ψ) → ∀x∀y(∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃zψ)) |
13 | 10, 12 | syl 14 |
. . . 4
⊢ (∀x∀y∀zφ → ∀x∀y(∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃zψ)) |
14 | | exim 1487 |
. . . . 5
⊢ (∀y(∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃zψ) → (∃y∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃y∃zψ)) |
15 | 14 | alimi 1341 |
. . . 4
⊢ (∀x∀y(∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃zψ) → ∀x(∃y∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃y∃zψ)) |
16 | | exim 1487 |
. . . 4
⊢ (∀x(∃y∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃y∃zψ) → (∃x∃y∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃x∃y∃zψ)) |
17 | 13, 15, 16 | 3syl 17 |
. . 3
⊢ (∀x∀y∀zφ → (∃x∃y∃z(x = A ∧ y = B ∧ z = 𝐶) → ∃x∃y∃zψ)) |
18 | | 19.9v 1748 |
. . . 4
⊢ (∃x∃y∃zψ ↔ ∃y∃zψ) |
19 | | 19.9v 1748 |
. . . 4
⊢ (∃y∃zψ ↔ ∃zψ) |
20 | | 19.9v 1748 |
. . . 4
⊢ (∃zψ ↔ ψ) |
21 | 18, 19, 20 | 3bitri 195 |
. . 3
⊢ (∃x∃y∃zψ ↔ ψ) |
22 | 17, 21 | syl6ib 150 |
. 2
⊢ (∀x∀y∀zφ → (∃x∃y∃z(x = A ∧ y = B ∧ z = 𝐶) → ψ)) |
23 | 6, 22 | syl5com 26 |
1
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∀x∀y∀zφ → ψ)) |