Step | Hyp | Ref
| Expression |
1 | | vprc 3879 |
. . . 4
⊢ ¬ V
∈ V |
2 | | vex 2554 |
. . . . . . . . . 10
⊢ z ∈
V |
3 | 2 | snid 3394 |
. . . . . . . . 9
⊢ z ∈ {z} |
4 | | a9ev 1584 |
. . . . . . . . . 10
⊢ ∃y y = z |
5 | | sneq 3378 |
. . . . . . . . . . 11
⊢ (z = y →
{z} = {y}) |
6 | 5 | equcoms 1591 |
. . . . . . . . . 10
⊢ (y = z →
{z} = {y}) |
7 | 4, 6 | eximii 1490 |
. . . . . . . . 9
⊢ ∃y{z} = {y} |
8 | | snexgOLD 3926 |
. . . . . . . . . . 11
⊢ (z ∈ V →
{z} ∈
V) |
9 | 2, 8 | ax-mp 7 |
. . . . . . . . . 10
⊢ {z} ∈
V |
10 | | eleq2 2098 |
. . . . . . . . . . 11
⊢ (x = {z} →
(z ∈
x ↔ z ∈ {z})) |
11 | | eqeq1 2043 |
. . . . . . . . . . . 12
⊢ (x = {z} →
(x = {y} ↔ {z} =
{y})) |
12 | 11 | exbidv 1703 |
. . . . . . . . . . 11
⊢ (x = {z} →
(∃y
x = {y}
↔ ∃y{z} = {y})) |
13 | 10, 12 | anbi12d 442 |
. . . . . . . . . 10
⊢ (x = {z} →
((z ∈
x ∧ ∃y x = {y}) ↔
(z ∈
{z} ∧
∃y{z} = {y}))) |
14 | 9, 13 | spcev 2641 |
. . . . . . . . 9
⊢
((z ∈ {z} ∧ ∃y{z} = {y}) → ∃x(z ∈ x ∧ ∃y x = {y})) |
15 | 3, 7, 14 | mp2an 402 |
. . . . . . . 8
⊢ ∃x(z ∈ x ∧ ∃y x = {y}) |
16 | | eluniab 3583 |
. . . . . . . 8
⊢ (z ∈ ∪ {x ∣ ∃y x = {y}} ↔
∃x(z ∈ x ∧ ∃y x = {y})) |
17 | 15, 16 | mpbir 134 |
. . . . . . 7
⊢ z ∈ ∪ {x ∣ ∃y x = {y}} |
18 | 17, 2 | 2th 163 |
. . . . . 6
⊢ (z ∈ ∪ {x ∣ ∃y x = {y}} ↔
z ∈
V) |
19 | 18 | eqriv 2034 |
. . . . 5
⊢ ∪ {x ∣ ∃y x = {y}} =
V |
20 | 19 | eleq1i 2100 |
. . . 4
⊢ (∪ {x ∣ ∃y x = {y}} ∈ V ↔ V ∈
V) |
21 | 1, 20 | mtbir 595 |
. . 3
⊢ ¬
∪ {x ∣
∃y
x = {y}} ∈
V |
22 | | uniexg 4141 |
. . 3
⊢
({x ∣ ∃y x = {y}} ∈ V → ∪ {x ∣ ∃y x = {y}} ∈ V) |
23 | 21, 22 | mto 587 |
. 2
⊢ ¬
{x ∣ ∃y x = {y}} ∈ V |
24 | 23 | nelir 2294 |
1
⊢ {x ∣ ∃y x = {y}} ∉
V |