Step | Hyp | Ref
| Expression |
1 | | vprc 4724 |
. . . 4
⊢ ¬ V
∈ V |
2 | | vsnid 4156 |
. . . . . . . . 9
⊢ 𝑧 ∈ {𝑧} |
3 | | ax6ev 1877 |
. . . . . . . . . 10
⊢
∃𝑦 𝑦 = 𝑧 |
4 | | sneq 4135 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → {𝑧} = {𝑦}) |
5 | 4 | equcoms 1934 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → {𝑧} = {𝑦}) |
6 | 3, 5 | eximii 1754 |
. . . . . . . . 9
⊢
∃𝑦{𝑧} = {𝑦} |
7 | | snex 4835 |
. . . . . . . . . 10
⊢ {𝑧} ∈ V |
8 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑧} → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ {𝑧})) |
9 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑥 = {𝑧} → (𝑥 = {𝑦} ↔ {𝑧} = {𝑦})) |
10 | 9 | exbidv 1837 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑧} → (∃𝑦 𝑥 = {𝑦} ↔ ∃𝑦{𝑧} = {𝑦})) |
11 | 8, 10 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑧} → ((𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦}) ↔ (𝑧 ∈ {𝑧} ∧ ∃𝑦{𝑧} = {𝑦}))) |
12 | 7, 11 | spcev 3273 |
. . . . . . . . 9
⊢ ((𝑧 ∈ {𝑧} ∧ ∃𝑦{𝑧} = {𝑦}) → ∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦})) |
13 | 2, 6, 12 | mp2an 704 |
. . . . . . . 8
⊢
∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦}) |
14 | | eluniab 4383 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ↔ ∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦})) |
15 | 13, 14 | mpbir 220 |
. . . . . . 7
⊢ 𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} |
16 | | vex 3176 |
. . . . . . 7
⊢ 𝑧 ∈ V |
17 | 15, 16 | 2th 253 |
. . . . . 6
⊢ (𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ↔ 𝑧 ∈ V) |
18 | 17 | eqriv 2607 |
. . . . 5
⊢ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} = V |
19 | 18 | eleq1i 2679 |
. . . 4
⊢ (∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ∈ V ↔ V ∈
V) |
20 | 1, 19 | mtbir 312 |
. . 3
⊢ ¬
∪ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∈ V |
21 | | uniexg 6853 |
. . 3
⊢ ({𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∈ V → ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ∈ V) |
22 | 20, 21 | mto 187 |
. 2
⊢ ¬
{𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∈ V |
23 | 22 | nelir 2886 |
1
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V |