Proof of Theorem nfsb4t
Step | Hyp | Ref
| Expression |
1 | | sbequ12 2111 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
2 | 1 | sps 2055 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
3 | 2 | drnf2 2330 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
4 | 3 | biimpd 219 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
5 | 4 | spsd 2057 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
6 | 5 | impcom 446 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
7 | 6 | a1d 25 |
. 2
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
8 | | nfnf1 2031 |
. . . . 5
⊢
Ⅎ𝑧Ⅎ𝑧𝜑 |
9 | 8 | nfal 2153 |
. . . 4
⊢
Ⅎ𝑧∀𝑥Ⅎ𝑧𝜑 |
10 | | nfnae 2318 |
. . . 4
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑦 |
11 | 9, 10 | nfan 1828 |
. . 3
⊢
Ⅎ𝑧(∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
12 | | nfa1 2028 |
. . . 4
⊢
Ⅎ𝑥∀𝑥Ⅎ𝑧𝜑 |
13 | | nfnae 2318 |
. . . 4
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
14 | 12, 13 | nfan 1828 |
. . 3
⊢
Ⅎ𝑥(∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
15 | | sp 2053 |
. . . 4
⊢
(∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧𝜑) |
16 | 15 | adantr 481 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜑) |
17 | | nfsb2 2360 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) |
18 | 17 | adantl 482 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥[𝑦 / 𝑥]𝜑) |
19 | 1 | a1i 11 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))) |
20 | 11, 14, 16, 18, 19 | dvelimdf 2335 |
. 2
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
21 | 7, 20 | pm2.61dan 832 |
1
⊢
(∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |