NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  vvex GIF version

Theorem vvex 4109
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.)
Assertion
Ref Expression
vvex V V

Proof of Theorem vvex
StepHypRef Expression
1 uncompl 4074 . 2 (x ∪ ∼ x) = V
2 vex 2862 . . 3 x V
32complex 4104 . . 3 x V
42, 3unex 4106 . 2 (x ∪ ∼ x) V
51, 4eqeltrri 2424 1 V V
Colors of variables: wff setvar class
Syntax hints:   wcel 1710  Vcvv 2859  ccompl 3205  cun 3207
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 4078
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 2478  df-v 2861  df-nin 3211  df-compl 3212  df-un 3214
This theorem is referenced by:  0ex  4110  cnvkexg  4286  uni1exg  4292  ssetkex  4294  imakexg  4299  pw1exg  4302  ins2kexg  4305  ins3kexg  4306  cokexg  4309  imagekexg  4311  abexv  4324  pwexg  4328  nnsucelrlem1  4424  preaddccan1lem1  4454  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  4728  1stex  4732  swapex  4735  ssetex  4737  imaexg  4739  coexg  4742  siexg  4745  rnexg  5138  resexg  5150  ins2exg  5831  ins3exg  5832  imageexg  5836  mptexlem  5849  mpt2exlem  5850  cupex  5855  disjex  5858  addcfnex  5859  funsex  5863  fnsex  5867  crossex  5887  domfnex  5907  ranfnex  5908  transex  5947  refex  5948  antisymex  5949  connexex  5950  foundex  5951  extex  5952  symex  5953  ider  5980  ssetpov  5981  eqer  5998  enex  6069  ener  6077  enpw1lem1  6098  enmap2lem1  6100  enmap1lem1  6106  enpw  6124  ncsex  6148  ncpw1c  6192  1p1e2c  6193  2p1e3c  6194  ce0addcnnul  6217  ce2  6230  ce2nc1  6231  lecncvg  6237  tcncv  6263  tcfnex  6281  ncvsq  6293  vvsqenvv  6294  csucex  6296  addccan2nclem2  6301  nmembers1lem1  6305  nncdiv3lem2  6312  spacvallem1  6317  nchoicelem11  6335  nchoicelem19  6343  fnfreclem1  6355
  Copyright terms: Public domain W3C validator