Step | Hyp | Ref
| Expression |
1 | | alexnim 1536 |
. 2
⊢ (∀x∃y ¬
y ∈
x → ¬ ∃x∀y y ∈ x) |
2 | | ax-bdel 9276 |
. . . . 5
⊢
BOUNDED z ∈ z |
3 | 2 | ax-bdn 9272 |
. . . 4
⊢
BOUNDED ¬ z ∈ z |
4 | 3 | bdsep1 9340 |
. . 3
⊢ ∃y∀z(z ∈ y ↔ (z
∈ x ∧ ¬ z ∈ z)) |
5 | | elequ1 1597 |
. . . . . 6
⊢ (z = y →
(z ∈
y ↔ y ∈ y)) |
6 | | elequ1 1597 |
. . . . . . 7
⊢ (z = y →
(z ∈
x ↔ y ∈ x)) |
7 | | elequ1 1597 |
. . . . . . . . 9
⊢ (z = y →
(z ∈
z ↔ y ∈ z)) |
8 | | elequ2 1598 |
. . . . . . . . 9
⊢ (z = y →
(y ∈
z ↔ y ∈ y)) |
9 | 7, 8 | bitrd 177 |
. . . . . . . 8
⊢ (z = y →
(z ∈
z ↔ y ∈ y)) |
10 | 9 | notbid 591 |
. . . . . . 7
⊢ (z = y →
(¬ z ∈ z ↔
¬ y ∈
y)) |
11 | 6, 10 | anbi12d 442 |
. . . . . 6
⊢ (z = y →
((z ∈
x ∧ ¬
z ∈
z) ↔ (y ∈ x ∧ ¬ y ∈ y))) |
12 | 5, 11 | bibi12d 224 |
. . . . 5
⊢ (z = y →
((z ∈
y ↔ (z ∈ x ∧ ¬ z ∈ z)) ↔ (y
∈ y
↔ (y ∈ x ∧ ¬ y ∈ y)))) |
13 | 12 | spv 1737 |
. . . 4
⊢ (∀z(z ∈ y ↔ (z
∈ x ∧ ¬ z ∈ z)) →
(y ∈
y ↔ (y ∈ x ∧ ¬ y ∈ y))) |
14 | | pclem6 1264 |
. . . 4
⊢
((y ∈ y ↔
(y ∈
x ∧ ¬
y ∈
y)) → ¬ y ∈ x) |
15 | 13, 14 | syl 14 |
. . 3
⊢ (∀z(z ∈ y ↔ (z
∈ x ∧ ¬ z ∈ z)) →
¬ y ∈
x) |
16 | 4, 15 | eximii 1490 |
. 2
⊢ ∃y ¬
y ∈
x |
17 | 1, 16 | mpg 1337 |
1
⊢ ¬
∃x∀y y ∈ x |