Proof of Theorem spc3egv
Step | Hyp | Ref
| Expression |
1 | | elex 3449 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | elex 3449 |
. 2
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) |
3 | | elex 3449 |
. 2
⊢ (𝐶 ∈ 𝑋 → 𝐶 ∈ V) |
4 | | simp1 1135 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → 𝐴 ∈ V) |
5 | | spc3egv.1 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → (𝜑 ↔ 𝜓)) |
6 | 5 | 3coml 1126 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓)) |
7 | 6 | 3expa 1117 |
. . . . . . . . 9
⊢ (((𝑦 = 𝐵 ∧ 𝑧 = 𝐶) ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓)) |
8 | 7 | pm5.74da 801 |
. . . . . . . 8
⊢ ((𝑦 = 𝐵 ∧ 𝑧 = 𝐶) → ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))) |
9 | 8 | spc2egv 3537 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → ((𝑥 = 𝐴 → 𝜓) → ∃𝑦∃𝑧(𝑥 = 𝐴 → 𝜑))) |
10 | | 19.37v 1999 |
. . . . . . . . 9
⊢
(∃𝑧(𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → ∃𝑧𝜑)) |
11 | 10 | exbii 1854 |
. . . . . . . 8
⊢
(∃𝑦∃𝑧(𝑥 = 𝐴 → 𝜑) ↔ ∃𝑦(𝑥 = 𝐴 → ∃𝑧𝜑)) |
12 | | 19.37v 1999 |
. . . . . . . 8
⊢
(∃𝑦(𝑥 = 𝐴 → ∃𝑧𝜑) ↔ (𝑥 = 𝐴 → ∃𝑦∃𝑧𝜑)) |
13 | 11, 12 | bitri 274 |
. . . . . . 7
⊢
(∃𝑦∃𝑧(𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → ∃𝑦∃𝑧𝜑)) |
14 | 9, 13 | syl6ib 250 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → ((𝑥 = 𝐴 → 𝜓) → (𝑥 = 𝐴 → ∃𝑦∃𝑧𝜑))) |
15 | 14 | pm2.86d 108 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝑥 = 𝐴 → (𝜓 → ∃𝑦∃𝑧𝜑))) |
16 | 15 | 3adant1 1129 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝑥 = 𝐴 → (𝜓 → ∃𝑦∃𝑧𝜑))) |
17 | 16 | imp 407 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑥 = 𝐴) → (𝜓 → ∃𝑦∃𝑧𝜑)) |
18 | 4, 17 | spcimedv 3533 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑)) |
19 | 1, 2, 3, 18 | syl3an 1159 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝜓 → ∃𝑥∃𝑦∃𝑧𝜑)) |