| Step | Hyp | Ref
| Expression |
| 1 | | eu6 2574 |
. . . 4
⊢
(∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
| 2 | 1 | biimpi 216 |
. . 3
⊢
(∃!𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) |
| 3 | | iota4 6542 |
. . 3
⊢
(∃!𝑥𝜑 → [(℩𝑥𝜑) / 𝑥]𝜑) |
| 4 | | iotaval 6532 |
. . . . . 6
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → (℩𝑥𝜑) = 𝑦) |
| 5 | 4 | eqcomd 2743 |
. . . . 5
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → 𝑦 = (℩𝑥𝜑)) |
| 6 | | spsbim 2072 |
. . . . . . . 8
⊢
(∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) |
| 7 | | sbsbc 3792 |
. . . . . . . 8
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
| 8 | | sbsbc 3792 |
. . . . . . . 8
⊢ ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓) |
| 9 | 6, 7, 8 | 3imtr3g 295 |
. . . . . . 7
⊢
(∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) |
| 10 | | dfsbcq 3790 |
. . . . . . . 8
⊢ (𝑦 = (℩𝑥𝜑) → ([𝑦 / 𝑥]𝜑 ↔ [(℩𝑥𝜑) / 𝑥]𝜑)) |
| 11 | | dfsbcq 3790 |
. . . . . . . 8
⊢ (𝑦 = (℩𝑥𝜑) → ([𝑦 / 𝑥]𝜓 ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) |
| 12 | 10, 11 | imbi12d 344 |
. . . . . . 7
⊢ (𝑦 = (℩𝑥𝜑) → (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) ↔ ([(℩𝑥𝜑) / 𝑥]𝜑 → [(℩𝑥𝜑) / 𝑥]𝜓))) |
| 13 | 9, 12 | imbitrid 244 |
. . . . . 6
⊢ (𝑦 = (℩𝑥𝜑) → (∀𝑥(𝜑 → 𝜓) → ([(℩𝑥𝜑) / 𝑥]𝜑 → [(℩𝑥𝜑) / 𝑥]𝜓))) |
| 14 | 13 | com23 86 |
. . . . 5
⊢ (𝑦 = (℩𝑥𝜑) → ([(℩𝑥𝜑) / 𝑥]𝜑 → (∀𝑥(𝜑 → 𝜓) → [(℩𝑥𝜑) / 𝑥]𝜓))) |
| 15 | 5, 14 | syl 17 |
. . . 4
⊢
(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([(℩𝑥𝜑) / 𝑥]𝜑 → (∀𝑥(𝜑 → 𝜓) → [(℩𝑥𝜑) / 𝑥]𝜓))) |
| 16 | 15 | exlimiv 1930 |
. . 3
⊢
(∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([(℩𝑥𝜑) / 𝑥]𝜑 → (∀𝑥(𝜑 → 𝜓) → [(℩𝑥𝜑) / 𝑥]𝜓))) |
| 17 | 2, 3, 16 | sylc 65 |
. 2
⊢
(∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → [(℩𝑥𝜑) / 𝑥]𝜓)) |
| 18 | | iotaexeu 44437 |
. . . . 5
⊢
(∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V) |
| 19 | 10, 11 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑦 = (℩𝑥𝜑) → (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) ↔ ([(℩𝑥𝜑) / 𝑥]𝜑 ∧ [(℩𝑥𝜑) / 𝑥]𝜓))) |
| 20 | 19 | imbi1d 341 |
. . . . . . 7
⊢ (𝑦 = (℩𝑥𝜑) → ((([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) ↔ (([(℩𝑥𝜑) / 𝑥]𝜑 ∧ [(℩𝑥𝜑) / 𝑥]𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))) |
| 21 | | sbcan 3838 |
. . . . . . . 8
⊢
([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
| 22 | | spesbc 3882 |
. . . . . . . 8
⊢
([𝑦 / 𝑥](𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
| 23 | 21, 22 | sylbir 235 |
. . . . . . 7
⊢
(([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
| 24 | 20, 23 | vtoclg 3554 |
. . . . . 6
⊢
((℩𝑥𝜑) ∈ V →
(([(℩𝑥𝜑) / 𝑥]𝜑 ∧ [(℩𝑥𝜑) / 𝑥]𝜓) → ∃𝑥(𝜑 ∧ 𝜓))) |
| 25 | 24 | expd 415 |
. . . . 5
⊢
((℩𝑥𝜑) ∈ V →
([(℩𝑥𝜑) / 𝑥]𝜑 → ([(℩𝑥𝜑) / 𝑥]𝜓 → ∃𝑥(𝜑 ∧ 𝜓)))) |
| 26 | 18, 3, 25 | sylc 65 |
. . . 4
⊢
(∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑥]𝜓 → ∃𝑥(𝜑 ∧ 𝜓))) |
| 27 | 26 | anc2li 555 |
. . 3
⊢
(∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑥]𝜓 → (∃!𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)))) |
| 28 | | eupicka 2634 |
. . 3
⊢
((∃!𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → ∀𝑥(𝜑 → 𝜓)) |
| 29 | 27, 28 | syl6 35 |
. 2
⊢
(∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑥]𝜓 → ∀𝑥(𝜑 → 𝜓))) |
| 30 | 17, 29 | impbid 212 |
1
⊢
(∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓)) |