Step | Hyp | Ref
| Expression |
1 | | df-eu 2462 |
. . . 4
⊢
(∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
2 | 1 | biimpi 205 |
. . 3
⊢
(∃!𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
3 | | iota4 5786 |
. . 3
⊢
(∃!𝑥𝜑 → [(℩𝑥𝜑) / 𝑥]𝜑) |
4 | | iotaval 5779 |
. . . . . 6
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦) |
5 | 4 | eqcomd 2616 |
. . . . 5
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → 𝑦 = (℩𝑥𝜑)) |
6 | | spsbim 2382 |
. . . . . . . 8
⊢
(∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) |
7 | | sbsbc 3406 |
. . . . . . . 8
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
8 | | sbsbc 3406 |
. . . . . . . 8
⊢ ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓) |
9 | 6, 7, 8 | 3imtr3g 283 |
. . . . . . 7
⊢
(∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) |
10 | | dfsbcq 3404 |
. . . . . . . 8
⊢ (𝑦 = (℩𝑥𝜑) → ([𝑦 / 𝑥]𝜑 ↔ [(℩𝑥𝜑) / 𝑥]𝜑)) |
11 | | dfsbcq 3404 |
. . . . . . . 8
⊢ (𝑦 = (℩𝑥𝜑) → ([𝑦 / 𝑥]𝜓 ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) |
12 | 10, 11 | imbi12d 333 |
. . . . . . 7
⊢ (𝑦 = (℩𝑥𝜑) → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([(℩𝑥𝜑) / 𝑥]𝜑 → [(℩𝑥𝜑) / 𝑥]𝜓))) |
13 | 9, 12 | syl5ib 233 |
. . . . . 6
⊢ (𝑦 = (℩𝑥𝜑) → (∀𝑥(𝜑 → 𝜓) → ([(℩𝑥𝜑) / 𝑥]𝜑 → [(℩𝑥𝜑) / 𝑥]𝜓))) |
14 | 13 | com23 84 |
. . . . 5
⊢ (𝑦 = (℩𝑥𝜑) → ([(℩𝑥𝜑) / 𝑥]𝜑 → (∀𝑥(𝜑 → 𝜓) → [(℩𝑥𝜑) / 𝑥]𝜓))) |
15 | 5, 14 | syl 17 |
. . . 4
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([(℩𝑥𝜑) / 𝑥]𝜑 → (∀𝑥(𝜑 → 𝜓) → [(℩𝑥𝜑) / 𝑥]𝜓))) |
16 | 15 | exlimiv 1845 |
. . 3
⊢
(∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([(℩𝑥𝜑) / 𝑥]𝜑 → (∀𝑥(𝜑 → 𝜓) → [(℩𝑥𝜑) / 𝑥]𝜓))) |
17 | 2, 3, 16 | sylc 63 |
. 2
⊢
(∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → [(℩𝑥𝜑) / 𝑥]𝜓)) |
18 | | iotaexeu 37641 |
. . . . 5
⊢
(∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V) |
19 | 10, 11 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑦 = (℩𝑥𝜑) → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([(℩𝑥𝜑) / 𝑥]𝜑 ∧ [(℩𝑥𝜑) / 𝑥]𝜓))) |
20 | 19 | imbi1d 330 |
. . . . . . 7
⊢ (𝑦 = (℩𝑥𝜑) → ((([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) ↔ (([(℩𝑥𝜑) / 𝑥]𝜑 ∧ [(℩𝑥𝜑) / 𝑥]𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))) |
21 | | sbcan 3445 |
. . . . . . . 8
⊢
([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
22 | | spesbc 3487 |
. . . . . . . 8
⊢
([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
23 | 21, 22 | sylbir 224 |
. . . . . . 7
⊢
(([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
24 | 20, 23 | vtoclg 3239 |
. . . . . 6
⊢
((℩𝑥𝜑) ∈ V →
(([(℩𝑥𝜑) / 𝑥]𝜑 ∧ [(℩𝑥𝜑) / 𝑥]𝜓) → ∃𝑥(𝜑 ∧ 𝜓))) |
25 | 24 | expd 451 |
. . . . 5
⊢
((℩𝑥𝜑) ∈ V →
([(℩𝑥𝜑) / 𝑥]𝜑 → ([(℩𝑥𝜑) / 𝑥]𝜓 → ∃𝑥(𝜑 ∧ 𝜓)))) |
26 | 18, 3, 25 | sylc 63 |
. . . 4
⊢
(∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑥]𝜓 → ∃𝑥(𝜑 ∧ 𝜓))) |
27 | 26 | anc2li 578 |
. . 3
⊢
(∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑥]𝜓 → (∃!𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)))) |
28 | | eupicka 2525 |
. . 3
⊢
((∃!𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → ∀𝑥(𝜑 → 𝜓)) |
29 | 27, 28 | syl6 34 |
. 2
⊢
(∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑥]𝜓 → ∀𝑥(𝜑 → 𝜓))) |
30 | 17, 29 | impbid 201 |
1
⊢
(∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) |