| Step | Hyp | Ref
| Expression |
| 1 | | df-riota 7388 |
. 2
⊢
(℩𝑦
∈ 𝐴 𝜓) = (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) |
| 2 | | nfriotadw.1 |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
| 3 | | nfnaew 2149 |
. . . . . 6
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
| 4 | 2, 3 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑦(𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
| 5 | | nfcvd 2906 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
| 6 | 5 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝑦) |
| 7 | | nfriotadw.3 |
. . . . . . . 8
⊢ (𝜑 → Ⅎ𝑥𝐴) |
| 8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝐴) |
| 9 | 6, 8 | nfeld 2917 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥 𝑦 ∈ 𝐴) |
| 10 | | nfriotadw.2 |
. . . . . . 7
⊢ (𝜑 → Ⅎ𝑥𝜓) |
| 11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) |
| 12 | 9, 11 | nfand 1897 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝜓)) |
| 13 | 4, 12 | nfiotadw 6517 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥(℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 14 | 13 | ex 412 |
. . 3
⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)))) |
| 15 | | nfiota1 6516 |
. . . 4
⊢
Ⅎ𝑦(℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) |
| 16 | | biidd 262 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑦 → (𝑤 ∈ (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ 𝑤 ∈ (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)))) |
| 17 | 16 | drnf1v 2375 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥 𝑤 ∈ (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ Ⅎ𝑦 𝑤 ∈ (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)))) |
| 18 | 17 | albidv 1920 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑤Ⅎ𝑥 𝑤 ∈ (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ ∀𝑤Ⅎ𝑦 𝑤 ∈ (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)))) |
| 19 | | df-nfc 2892 |
. . . . 5
⊢
(Ⅎ𝑥(℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ ∀𝑤Ⅎ𝑥 𝑤 ∈ (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 20 | | df-nfc 2892 |
. . . . 5
⊢
(Ⅎ𝑦(℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ ∀𝑤Ⅎ𝑦 𝑤 ∈ (℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 21 | 18, 19, 20 | 3bitr4g 314 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥(℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)) ↔ Ⅎ𝑦(℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓)))) |
| 22 | 15, 21 | mpbiri 258 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 23 | 14, 22 | pm2.61d2 181 |
. 2
⊢ (𝜑 → Ⅎ𝑥(℩𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))) |
| 24 | 1, 23 | nfcxfrd 2904 |
1
⊢ (𝜑 → Ⅎ𝑥(℩𝑦 ∈ 𝐴 𝜓)) |