Step | Hyp | Ref
| Expression |
1 | | dfnul4 4255 |
. . 3
⊢ ∅ =
{𝑥 ∣
⊥} |
2 | 1 | eqeq2i 2752 |
. 2
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ 𝜑} = {𝑥 ∣ ⊥}) |
3 | | dfcleq 2732 |
. 2
⊢ ({𝑥 ∣ 𝜑} = {𝑥 ∣ ⊥} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ⊥})) |
4 | | df-clab 2717 |
. . . . . 6
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) |
5 | | sb6 2093 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
6 | 4, 5 | bitri 278 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
7 | | df-clab 2717 |
. . . . . 6
⊢ (𝑦 ∈ {𝑥 ∣ ⊥} ↔ [𝑦 / 𝑥]⊥) |
8 | | sbv 2096 |
. . . . . 6
⊢ ([𝑦 / 𝑥]⊥ ↔ ⊥) |
9 | 7, 8 | bitri 278 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∣ ⊥} ↔
⊥) |
10 | 6, 9 | bibi12i 343 |
. . . 4
⊢ ((𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ⊥)) |
11 | 10 | albii 1827 |
. . 3
⊢
(∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}) ↔ ∀𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ⊥)) |
12 | | nbfal 1558 |
. . . . 5
⊢ (¬
∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ⊥)) |
13 | 12 | bicomi 227 |
. . . 4
⊢
((∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ⊥) ↔ ¬ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
14 | 13 | albii 1827 |
. . 3
⊢
(∀𝑦(∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ⊥) ↔ ∀𝑦 ¬ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
15 | | nfna1 2155 |
. . . 4
⊢
Ⅎ𝑥 ¬
∀𝑥(𝑥 = 𝑦 → 𝜑) |
16 | | nfv 1922 |
. . . 4
⊢
Ⅎ𝑦 ¬ 𝜑 |
17 | | pm2.27 42 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥 = 𝑦 → 𝜑) → 𝜑)) |
18 | 17 | spsd 2186 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜑)) |
19 | 18 | equcoms 2028 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜑)) |
20 | | ax12v 2178 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
21 | 20 | equcoms 2028 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
22 | 19, 21 | impbid 215 |
. . . . 5
⊢ (𝑦 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) |
23 | 22 | notbid 321 |
. . . 4
⊢ (𝑦 = 𝑥 → (¬ ∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ¬ 𝜑)) |
24 | 15, 16, 23 | cbvalv1 2343 |
. . 3
⊢
(∀𝑦 ¬
∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥 ¬ 𝜑) |
25 | 11, 14, 24 | 3bitri 300 |
. 2
⊢
(∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝜑) |
26 | 2, 3, 25 | 3bitri 300 |
1
⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) |