New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > vvex | GIF version |
Description: The universal class exists. This marks a major departure from ZFC set theory, where V is a proper class. (Contributed by SF, 12-Jan-2015.) |
Ref | Expression |
---|---|
vvex | ⊢ V ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uncompl 4075 | . 2 ⊢ (x ∪ ∼ x) = V | |
2 | vex 2863 | . . 3 ⊢ x ∈ V | |
3 | 2 | complex 4105 | . . 3 ⊢ ∼ x ∈ V |
4 | 2, 3 | unex 4107 | . 2 ⊢ (x ∪ ∼ x) ∈ V |
5 | 1, 4 | eqeltrri 2424 | 1 ⊢ V ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1710 Vcvv 2860 ∼ ccompl 3206 ∪ cun 3208 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-v 2862 df-nin 3212 df-compl 3213 df-un 3215 |
This theorem is referenced by: 0ex 4111 cnvkexg 4287 uni1exg 4293 ssetkex 4295 imakexg 4300 pw1exg 4303 ins2kexg 4306 ins3kexg 4307 cokexg 4310 imagekexg 4312 abexv 4325 pwexg 4329 nnsucelrlem1 4425 preaddccan2lem1 4455 ltfinex 4465 ssfin 4471 ncfinraiselem2 4481 ncfinlowerlem1 4483 tfinrelkex 4488 evenfinex 4504 oddfinex 4505 evenodddisjlem1 4516 nnadjoinlem1 4520 srelkex 4526 tfinnnlem1 4534 vfinspnn 4542 1cvsfin 4543 tncveqnc1fin 4545 vfintle 4547 vfinncvntnn 4549 phiexg 4572 opexg 4588 proj1exg 4592 proj2exg 4593 setconslem5 4736 1stex 4740 swapex 4743 ssetex 4745 imaexg 4747 coexg 4750 siexg 4753 rnexg 5105 resexg 5117 ins2exg 5796 ins3exg 5797 mptexlem 5811 mpt2exlem 5812 cupex 5817 composeex 5821 addcfnex 5825 fnsex 5833 crossex 5851 domfnex 5871 ranfnex 5872 transex 5911 foundex 5915 ider 5944 ssetpov 5945 eqer 5962 ener 6040 enmap2lem1 6064 enmap1lem1 6070 enpw 6088 ncsex 6112 ncpw1c 6155 1p1e2c 6156 2p1e3c 6157 ce0addcnnul 6180 ce2 6193 ce2nc1 6194 lecncvg 6200 tcncv 6227 tcfnex 6245 ncvsq 6257 vvsqenvv 6258 csucex 6260 addccan2nclem2 6265 nmembers1lem1 6269 nncdiv3lem2 6277 nchoicelem11 6300 nchoicelem19 6308 fnfreclem1 6318 |
Copyright terms: Public domain | W3C validator |