Step |
Hyp |
Ref |
Expression |
1 |
|
dvelimf.1 |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
dvelimf.2 |
⊢ Ⅎ 𝑧 𝜓 |
3 |
|
dvelimf.3 |
⊢ ( 𝑧 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) |
4 |
2 3
|
equsal |
⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ↔ 𝜓 ) |
5 |
4
|
bicomi |
⊢ ( 𝜓 ↔ ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) |
6 |
|
nfnae |
⊢ Ⅎ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 |
7 |
|
nfeqf |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑧 = 𝑦 ) |
8 |
7
|
ancoms |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑧 = 𝑦 ) |
9 |
1
|
a1i |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝜑 ) |
10 |
8 9
|
nfimd |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( 𝑧 = 𝑦 → 𝜑 ) ) |
11 |
6 10
|
nfald2 |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ∀ 𝑧 ( 𝑧 = 𝑦 → 𝜑 ) ) |
12 |
5 11
|
nfxfrd |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝜓 ) |