Proof of Theorem nfsb4t
Step | Hyp | Ref
| Expression |
1 | | sbequ12 2243 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
2 | 1 | sps 2174 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
3 | 2 | drnf2 2458 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
4 | 3 | biimpd 230 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
5 | 4 | spsd 2176 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑦 → (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
6 | 5 | impcom 408 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧[𝑦 / 𝑥]𝜑) |
7 | 6 | a1d 25 |
. 2
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ∀𝑥 𝑥 = 𝑦) → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
8 | | nfnf1 2149 |
. . . . 5
⊢
Ⅎ𝑧Ⅎ𝑧𝜑 |
9 | 8 | nfal 2333 |
. . . 4
⊢
Ⅎ𝑧∀𝑥Ⅎ𝑧𝜑 |
10 | | nfnae 2448 |
. . . 4
⊢
Ⅎ𝑧 ¬
∀𝑥 𝑥 = 𝑦 |
11 | 9, 10 | nfan 1891 |
. . 3
⊢
Ⅎ𝑧(∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
12 | | nfa1 2146 |
. . . 4
⊢
Ⅎ𝑥∀𝑥Ⅎ𝑧𝜑 |
13 | | nfnae 2448 |
. . . 4
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
14 | 12, 13 | nfan 1891 |
. . 3
⊢
Ⅎ𝑥(∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
15 | | sp 2172 |
. . . 4
⊢
(∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧𝜑) |
16 | 15 | adantr 481 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑧𝜑) |
17 | | nfsb2 2515 |
. . . 4
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) |
18 | 17 | adantl 482 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥[𝑦 / 𝑥]𝜑) |
19 | 1 | a1i 11 |
. . 3
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))) |
20 | 11, 14, 16, 18, 19 | dvelimdf 2463 |
. 2
⊢
((∀𝑥Ⅎ𝑧𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |
21 | 7, 20 | pm2.61dan 809 |
1
⊢
(∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) |