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