Step |
Hyp |
Ref |
Expression |
1 |
|
nmo.1 |
⊢ Ⅎ 𝑦 𝜑 |
2 |
1
|
mof |
⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) |
3 |
2
|
notbii |
⊢ ( ¬ ∃* 𝑥 𝜑 ↔ ¬ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) |
4 |
|
alnex |
⊢ ( ∀ 𝑦 ¬ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ¬ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) |
5 |
|
exnal |
⊢ ( ∃ 𝑥 ¬ ( 𝜑 → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) |
6 |
|
pm4.61 |
⊢ ( ¬ ( 𝜑 → 𝑥 = 𝑦 ) ↔ ( 𝜑 ∧ ¬ 𝑥 = 𝑦 ) ) |
7 |
|
biid |
⊢ ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 ) |
8 |
7
|
necon3bbii |
⊢ ( ¬ 𝑥 = 𝑦 ↔ 𝑥 ≠ 𝑦 ) |
9 |
8
|
anbi2i |
⊢ ( ( 𝜑 ∧ ¬ 𝑥 = 𝑦 ) ↔ ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) ) |
10 |
6 9
|
bitri |
⊢ ( ¬ ( 𝜑 → 𝑥 = 𝑦 ) ↔ ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) ) |
11 |
10
|
exbii |
⊢ ( ∃ 𝑥 ¬ ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) ) |
12 |
5 11
|
bitr3i |
⊢ ( ¬ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∃ 𝑥 ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) ) |
13 |
12
|
albii |
⊢ ( ∀ 𝑦 ¬ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) ) |
14 |
3 4 13
|
3bitr2i |
⊢ ( ¬ ∃* 𝑥 𝜑 ↔ ∀ 𝑦 ∃ 𝑥 ( 𝜑 ∧ 𝑥 ≠ 𝑦 ) ) |