Step | Hyp | Ref
| Expression |
1 | | vprc 4121 |
. . . 4
⊢ ¬ V
∈ V |
2 | | vsnid 3615 |
. . . . . . . . 9
⊢ 𝑧 ∈ {𝑧} |
3 | | a9ev 1690 |
. . . . . . . . . 10
⊢
∃𝑦 𝑦 = 𝑧 |
4 | | sneq 3594 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → {𝑧} = {𝑦}) |
5 | 4 | equcoms 1701 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → {𝑧} = {𝑦}) |
6 | 3, 5 | eximii 1595 |
. . . . . . . . 9
⊢
∃𝑦{𝑧} = {𝑦} |
7 | | vex 2733 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
8 | 7 | snex 4171 |
. . . . . . . . . 10
⊢ {𝑧} ∈ V |
9 | | eleq2 2234 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑧} → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ {𝑧})) |
10 | | eqeq1 2177 |
. . . . . . . . . . . 12
⊢ (𝑥 = {𝑧} → (𝑥 = {𝑦} ↔ {𝑧} = {𝑦})) |
11 | 10 | exbidv 1818 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑧} → (∃𝑦 𝑥 = {𝑦} ↔ ∃𝑦{𝑧} = {𝑦})) |
12 | 9, 11 | anbi12d 470 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑧} → ((𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦}) ↔ (𝑧 ∈ {𝑧} ∧ ∃𝑦{𝑧} = {𝑦}))) |
13 | 8, 12 | spcev 2825 |
. . . . . . . . 9
⊢ ((𝑧 ∈ {𝑧} ∧ ∃𝑦{𝑧} = {𝑦}) → ∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦})) |
14 | 2, 6, 13 | mp2an 424 |
. . . . . . . 8
⊢
∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦}) |
15 | | eluniab 3808 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ↔ ∃𝑥(𝑧 ∈ 𝑥 ∧ ∃𝑦 𝑥 = {𝑦})) |
16 | 14, 15 | mpbir 145 |
. . . . . . 7
⊢ 𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} |
17 | 16, 7 | 2th 173 |
. . . . . 6
⊢ (𝑧 ∈ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ↔ 𝑧 ∈ V) |
18 | 17 | eqriv 2167 |
. . . . 5
⊢ ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} = V |
19 | 18 | eleq1i 2236 |
. . . 4
⊢ (∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ∈ V ↔ V ∈
V) |
20 | 1, 19 | mtbir 666 |
. . 3
⊢ ¬
∪ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∈ V |
21 | | uniexg 4424 |
. . 3
⊢ ({𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∈ V → ∪ {𝑥
∣ ∃𝑦 𝑥 = {𝑦}} ∈ V) |
22 | 20, 21 | mto 657 |
. 2
⊢ ¬
{𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∈ V |
23 | 22 | nelir 2438 |
1
⊢ {𝑥 ∣ ∃𝑦 𝑥 = {𝑦}} ∉ V |