Proof of Theorem exdistrfor
Step | Hyp | Ref
| Expression |
1 | | exdistrfor.1 |
. 2
⊢
(∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥Ⅎ𝑦𝜑) |
2 | | biidd 171 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜓))) |
3 | 2 | drex1 1791 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑦(𝜑 ∧ 𝜓))) |
4 | 3 | drex2 1725 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥∃𝑦(𝜑 ∧ 𝜓))) |
5 | | hbe1 1488 |
. . . . . 6
⊢
(∃𝑥(𝜑 ∧ 𝜓) → ∀𝑥∃𝑥(𝜑 ∧ 𝜓)) |
6 | 5 | 19.9h 1636 |
. . . . 5
⊢
(∃𝑥∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ 𝜓)) |
7 | | 19.8a 1583 |
. . . . . . 7
⊢ (𝜓 → ∃𝑦𝜓) |
8 | 7 | anim2i 340 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ ∃𝑦𝜓)) |
9 | 8 | eximi 1593 |
. . . . 5
⊢
(∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) |
10 | 6, 9 | sylbi 120 |
. . . 4
⊢
(∃𝑥∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) |
11 | 4, 10 | syl6bir 163 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓))) |
12 | | ax-ial 1527 |
. . . 4
⊢
(∀𝑥Ⅎ𝑦𝜑 → ∀𝑥∀𝑥Ⅎ𝑦𝜑) |
13 | | 19.40 1624 |
. . . . . 6
⊢
(∃𝑦(𝜑 ∧ 𝜓) → (∃𝑦𝜑 ∧ ∃𝑦𝜓)) |
14 | | 19.9t 1635 |
. . . . . . . 8
⊢
(Ⅎ𝑦𝜑 → (∃𝑦𝜑 ↔ 𝜑)) |
15 | 14 | biimpd 143 |
. . . . . . 7
⊢
(Ⅎ𝑦𝜑 → (∃𝑦𝜑 → 𝜑)) |
16 | 15 | anim1d 334 |
. . . . . 6
⊢
(Ⅎ𝑦𝜑 → ((∃𝑦𝜑 ∧ ∃𝑦𝜓) → (𝜑 ∧ ∃𝑦𝜓))) |
17 | 13, 16 | syl5 32 |
. . . . 5
⊢
(Ⅎ𝑦𝜑 → (∃𝑦(𝜑 ∧ 𝜓) → (𝜑 ∧ ∃𝑦𝜓))) |
18 | 17 | sps 1530 |
. . . 4
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃𝑦(𝜑 ∧ 𝜓) → (𝜑 ∧ ∃𝑦𝜓))) |
19 | 12, 18 | eximdh 1604 |
. . 3
⊢
(∀𝑥Ⅎ𝑦𝜑 → (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓))) |
20 | 11, 19 | jaoi 711 |
. 2
⊢
((∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥Ⅎ𝑦𝜑) → (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓))) |
21 | 1, 20 | ax-mp 5 |
1
⊢
(∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) |