Step | Hyp | Ref
| Expression |
1 | | riota5f.3 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵)) |
2 | 1 | ralrimiva 2543 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝐵)) |
3 | | riota5f.2 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
4 | | a1tru 1364 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) → ⊤) |
5 | | reu6i 2921 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦)) → ∃!𝑥 ∈ 𝐴 𝜓) |
6 | 5 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) → ∃!𝑥 ∈ 𝐴 𝜓) |
7 | | nfv 1521 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝜑 |
8 | | nfv 1521 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
9 | | nfra1 2501 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦) |
10 | 8, 9 | nfan 1558 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦)) |
11 | 7, 10 | nfan 1558 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) |
12 | | nfcvd 2313 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) → Ⅎ𝑥𝑦) |
13 | | nfvd 1522 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) → Ⅎ𝑥⊤) |
14 | | simprl 526 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) → 𝑦 ∈ 𝐴) |
15 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → 𝑥 = 𝑦) |
16 | | simplrr 531 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦)) |
17 | | simplrl 530 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → 𝑦 ∈ 𝐴) |
18 | 15, 17 | eqeltrd 2247 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → 𝑥 ∈ 𝐴) |
19 | | rsp 2517 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝐴 (𝜓 ↔ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 → (𝜓 ↔ 𝑥 = 𝑦))) |
20 | 16, 18, 19 | sylc 62 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝑥 = 𝑦)) |
21 | 15, 20 | mpbird 166 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → 𝜓) |
22 | | a1tru 1364 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → ⊤) |
23 | 21, 22 | 2thd 174 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → (𝜓 ↔ ⊤)) |
24 | 11, 12, 13, 14, 23 | riota2df 5827 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) ∧ ∃!𝑥 ∈ 𝐴 𝜓) → (⊤ ↔
(℩𝑥 ∈
𝐴 𝜓) = 𝑦)) |
25 | 6, 24 | mpdan 419 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) → (⊤ ↔
(℩𝑥 ∈
𝐴 𝜓) = 𝑦)) |
26 | 4, 25 | mpbid 146 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦))) → (℩𝑥 ∈ 𝐴 𝜓) = 𝑦) |
27 | 26 | expr 373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦) → (℩𝑥 ∈ 𝐴 𝜓) = 𝑦)) |
28 | 27 | ralrimiva 2543 |
. . . 4
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦) → (℩𝑥 ∈ 𝐴 𝜓) = 𝑦)) |
29 | | rspsbc 3037 |
. . . 4
⊢ (𝐵 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦) → (℩𝑥 ∈ 𝐴 𝜓) = 𝑦) → [𝐵 / 𝑦](∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦) → (℩𝑥 ∈ 𝐴 𝜓) = 𝑦))) |
30 | 3, 28, 29 | sylc 62 |
. . 3
⊢ (𝜑 → [𝐵 / 𝑦](∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦) → (℩𝑥 ∈ 𝐴 𝜓) = 𝑦)) |
31 | | nfcvd 2313 |
. . . . . . . 8
⊢ (𝜑 → Ⅎ𝑥𝑦) |
32 | | riota5f.1 |
. . . . . . . 8
⊢ (𝜑 → Ⅎ𝑥𝐵) |
33 | 31, 32 | nfeqd 2327 |
. . . . . . 7
⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐵) |
34 | 7, 33 | nfan1 1557 |
. . . . . 6
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 = 𝐵) |
35 | | simpr 109 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
36 | 35 | eqeq2d 2182 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (𝑥 = 𝑦 ↔ 𝑥 = 𝐵)) |
37 | 36 | bibi2d 231 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → ((𝜓 ↔ 𝑥 = 𝑦) ↔ (𝜓 ↔ 𝑥 = 𝐵))) |
38 | 34, 37 | ralbid 2468 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝐵))) |
39 | 35 | eqeq2d 2182 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → ((℩𝑥 ∈ 𝐴 𝜓) = 𝑦 ↔ (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)) |
40 | 38, 39 | imbi12d 233 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = 𝐵) → ((∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦) → (℩𝑥 ∈ 𝐴 𝜓) = 𝑦) ↔ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝐵) → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵))) |
41 | 3, 40 | sbcied 2991 |
. . 3
⊢ (𝜑 → ([𝐵 / 𝑦](∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝑦) → (℩𝑥 ∈ 𝐴 𝜓) = 𝑦) ↔ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝐵) → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵))) |
42 | 30, 41 | mpbid 146 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝑥 = 𝐵) → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)) |
43 | 2, 42 | mpd 13 |
1
⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵) |