Proof of Theorem nfsb4tALT
Step | Hyp | Ref
| Expression |
1 | | dfsb1.p5 |
. . . . . . . . 9
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) |
2 | 1 | sbequ12ALT 2581 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃)) |
3 | 2 | sps 2184 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜃)) |
4 | 3 | drnf2 2466 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜃)) |
5 | 4 | biimpd 231 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 → Ⅎ𝑧𝜃)) |
6 | 5 | spsd 2186 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧𝜃)) |
7 | 6 | impcom 410 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜃) |
8 | 7 | a1d 25 |
. 2
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝜃)) |
9 | | nfnf1 2158 |
. . . . 5
⊢
Ⅎ𝑧Ⅎ𝑧𝜑 |
10 | 9 | nfal 2342 |
. . . 4
⊢
Ⅎ𝑧∀𝑥Ⅎ𝑧𝜑 |
11 | | nfnae 2456 |
. . . 4
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑦 |
12 | 10, 11 | nfan 1900 |
. . 3
⊢
Ⅎ𝑧(∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
13 | | nfa1 2155 |
. . . 4
⊢
Ⅎ𝑥∀𝑥Ⅎ𝑧𝜑 |
14 | | nfnae 2456 |
. . . 4
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
15 | 13, 14 | nfan 1900 |
. . 3
⊢
Ⅎ𝑥(∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
16 | | sp 2182 |
. . . 4
⊢
(∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧𝜑) |
17 | 16 | adantr 483 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜑) |
18 | 1 | nfsb2ALT 2600 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜃) |
19 | 18 | adantl 484 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜃) |
20 | 2 | a1i 11 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))) |
21 | 12, 15, 17, 19, 20 | dvelimdf 2471 |
. 2
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝜃)) |
22 | 8, 21 | pm2.61dan 811 |
1
⊢
(∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝜃)) |