Proof of Theorem euan
Step | Hyp | Ref
| Expression |
1 | | euan.1 |
. . . . . 6
⊢ (𝜑 → ∀𝑥𝜑) |
2 | | simpl 108 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝜑) |
3 | 1, 2 | exlimih 1573 |
. . . . 5
⊢
(∃𝑥(𝜑 ∧ 𝜓) → 𝜑) |
4 | 3 | adantr 274 |
. . . 4
⊢
((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃*𝑥(𝜑 ∧ 𝜓)) → 𝜑) |
5 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝜓) |
6 | 5 | eximi 1580 |
. . . . 5
⊢
(∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜓) |
7 | 6 | adantr 274 |
. . . 4
⊢
((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃*𝑥(𝜑 ∧ 𝜓)) → ∃𝑥𝜓) |
8 | | hbe1 1475 |
. . . . . 6
⊢
(∃𝑥(𝜑 ∧ 𝜓) → ∀𝑥∃𝑥(𝜑 ∧ 𝜓)) |
9 | 3 | a1d 22 |
. . . . . . . 8
⊢
(∃𝑥(𝜑 ∧ 𝜓) → (𝜓 → 𝜑)) |
10 | 9 | ancrd 324 |
. . . . . . 7
⊢
(∃𝑥(𝜑 ∧ 𝜓) → (𝜓 → (𝜑 ∧ 𝜓))) |
11 | 5, 10 | impbid2 142 |
. . . . . 6
⊢
(∃𝑥(𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ↔ 𝜓)) |
12 | 8, 11 | mobidh 2040 |
. . . . 5
⊢
(∃𝑥(𝜑 ∧ 𝜓) → (∃*𝑥(𝜑 ∧ 𝜓) ↔ ∃*𝑥𝜓)) |
13 | 12 | biimpa 294 |
. . . 4
⊢
((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃*𝑥(𝜑 ∧ 𝜓)) → ∃*𝑥𝜓) |
14 | 4, 7, 13 | jca32 308 |
. . 3
⊢
((∃𝑥(𝜑 ∧ 𝜓) ∧ ∃*𝑥(𝜑 ∧ 𝜓)) → (𝜑 ∧ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))) |
15 | | eu5 2053 |
. . 3
⊢
(∃!𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥(𝜑 ∧ 𝜓) ∧ ∃*𝑥(𝜑 ∧ 𝜓))) |
16 | | eu5 2053 |
. . . 4
⊢
(∃!𝑥𝜓 ↔ (∃𝑥𝜓 ∧ ∃*𝑥𝜓)) |
17 | 16 | anbi2i 453 |
. . 3
⊢ ((𝜑 ∧ ∃!𝑥𝜓) ↔ (𝜑 ∧ (∃𝑥𝜓 ∧ ∃*𝑥𝜓))) |
18 | 14, 15, 17 | 3imtr4i 200 |
. 2
⊢
(∃!𝑥(𝜑 ∧ 𝜓) → (𝜑 ∧ ∃!𝑥𝜓)) |
19 | | ibar 299 |
. . . 4
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
20 | 1, 19 | eubidh 2012 |
. . 3
⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥(𝜑 ∧ 𝜓))) |
21 | 20 | biimpa 294 |
. 2
⊢ ((𝜑 ∧ ∃!𝑥𝜓) → ∃!𝑥(𝜑 ∧ 𝜓)) |
22 | 18, 21 | impbii 125 |
1
⊢
(∃!𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥𝜓)) |