Proof of Theorem spc2gv
Step | Hyp | Ref
| Expression |
1 | | elisset 2562 |
. . . 4
⊢ (A ∈ 𝑉 → ∃x x = A) |
2 | | elisset 2562 |
. . . 4
⊢ (B ∈ 𝑊 → ∃y y = B) |
3 | 1, 2 | anim12i 321 |
. . 3
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → (∃x x = A ∧ ∃y y = B)) |
4 | | eeanv 1804 |
. . 3
⊢ (∃x∃y(x = A ∧ y = B) ↔ (∃x x = A ∧ ∃y y = B)) |
5 | 3, 4 | sylibr 137 |
. 2
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∃x∃y(x = A ∧ y = B)) |
6 | | spc2egv.1 |
. . . . . 6
⊢
((x = A ∧ y = B) →
(φ ↔ ψ)) |
7 | 6 | biimpcd 148 |
. . . . 5
⊢ (φ → ((x = A ∧ y = B) → ψ)) |
8 | 7 | 2alimi 1342 |
. . . 4
⊢ (∀x∀yφ → ∀x∀y((x = A ∧ y = B) → ψ)) |
9 | | exim 1487 |
. . . . 5
⊢ (∀y((x = A ∧ y = B) → ψ)
→ (∃y(x = A ∧ y = B) →
∃yψ)) |
10 | 9 | alimi 1341 |
. . . 4
⊢ (∀x∀y((x = A ∧ y = B) → ψ)
→ ∀x(∃y(x = A ∧ y = B) →
∃yψ)) |
11 | | exim 1487 |
. . . 4
⊢ (∀x(∃y(x = A ∧ y = B) → ∃yψ) → (∃x∃y(x = A ∧ y = B) → ∃x∃yψ)) |
12 | 8, 10, 11 | 3syl 17 |
. . 3
⊢ (∀x∀yφ → (∃x∃y(x = A ∧ y = B) → ∃x∃yψ)) |
13 | | 19.9v 1748 |
. . . 4
⊢ (∃x∃yψ ↔ ∃yψ) |
14 | | 19.9v 1748 |
. . . 4
⊢ (∃yψ ↔ ψ) |
15 | 13, 14 | bitri 173 |
. . 3
⊢ (∃x∃yψ ↔ ψ) |
16 | 12, 15 | syl6ib 150 |
. 2
⊢ (∀x∀yφ → (∃x∃y(x = A ∧ y = B) → ψ)) |
17 | 5, 16 | syl5com 26 |
1
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → (∀x∀yφ → ψ)) |