Proof of Theorem exdistrfor
Step | Hyp | Ref
| Expression |
1 | | exdistrfor.1 |
. 2
⊢ (∀x x = y ∨ ∀xℲyφ) |
2 | | biidd 161 |
. . . . . 6
⊢ (∀x x = y →
((φ ∧
ψ) ↔ (φ ∧ ψ))) |
3 | 2 | drex1 1676 |
. . . . 5
⊢ (∀x x = y →
(∃x(φ ∧ ψ) ↔
∃y(φ ∧ ψ))) |
4 | 3 | drex2 1617 |
. . . 4
⊢ (∀x x = y →
(∃x∃x(φ ∧ ψ) ↔ ∃x∃y(φ ∧ ψ))) |
5 | | hbe1 1381 |
. . . . . 6
⊢ (∃x(φ ∧ ψ) → ∀x∃x(φ ∧ ψ)) |
6 | 5 | 19.9h 1531 |
. . . . 5
⊢ (∃x∃x(φ ∧ ψ) ↔ ∃x(φ ∧ ψ)) |
7 | | 19.8a 1479 |
. . . . . . 7
⊢ (ψ → ∃yψ) |
8 | 7 | anim2i 324 |
. . . . . 6
⊢ ((φ ∧ ψ) → (φ ∧ ∃yψ)) |
9 | 8 | eximi 1488 |
. . . . 5
⊢ (∃x(φ ∧ ψ) → ∃x(φ ∧ ∃yψ)) |
10 | 6, 9 | sylbi 114 |
. . . 4
⊢ (∃x∃x(φ ∧ ψ) → ∃x(φ ∧ ∃yψ)) |
11 | 4, 10 | syl6bir 153 |
. . 3
⊢ (∀x x = y →
(∃x∃y(φ ∧ ψ) → ∃x(φ ∧ ∃yψ))) |
12 | | ax-ial 1424 |
. . . 4
⊢ (∀xℲyφ → ∀x∀xℲyφ) |
13 | | 19.40 1519 |
. . . . . 6
⊢ (∃y(φ ∧ ψ) → (∃yφ ∧ ∃yψ)) |
14 | | 19.9t 1530 |
. . . . . . . 8
⊢
(Ⅎyφ → (∃yφ ↔ φ)) |
15 | 14 | biimpd 132 |
. . . . . . 7
⊢
(Ⅎyφ → (∃yφ → φ)) |
16 | 15 | anim1d 319 |
. . . . . 6
⊢
(Ⅎyφ → ((∃yφ ∧ ∃yψ) → (φ ∧ ∃yψ))) |
17 | 13, 16 | syl5 28 |
. . . . 5
⊢
(Ⅎyφ → (∃y(φ ∧ ψ) → (φ ∧ ∃yψ))) |
18 | 17 | sps 1427 |
. . . 4
⊢ (∀xℲyφ → (∃y(φ ∧ ψ) → (φ ∧ ∃yψ))) |
19 | 12, 18 | eximdh 1499 |
. . 3
⊢ (∀xℲyφ → (∃x∃y(φ ∧ ψ) → ∃x(φ ∧ ∃yψ))) |
20 | 11, 19 | jaoi 635 |
. 2
⊢ ((∀x x = y ∨ ∀xℲyφ) → (∃x∃y(φ ∧ ψ) → ∃x(φ ∧ ∃yψ))) |
21 | 1, 20 | ax-mp 7 |
1
⊢ (∃x∃y(φ ∧ ψ) → ∃x(φ ∧ ∃yψ)) |