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

Step	Hyp	Ref	Expression
1		uncompl 4074	. 2 ⊢ (x ∪ ∼ x) = V
2		vex 2862	. . 3 ⊢ x ∈ V
3	2	complex 4104	. . 3 ⊢ ∼ x ∈ V
4	2, 3	unex 4106	. 2 ⊢ (x ∪ ∼ x) ∈ V
5	1, 4	eqeltrri 2424	1 ⊢ V ∈ V

Syntax hints:   ∈ wcel 1710  Vcvv 2859   ∼ ccompl 3205   ∪ cun 3207

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 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  preaddccan2lem1  4454  ltfinex  4464  ssfin  4470  ncfinraiselem2  4480  ncfinlowerlem1  4482  tfinrelkex  4487  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  srelkex  4525  tfinnnlem1  4533  vfinspnn  4541  1cvsfin  4542  tncveqnc1fin  4544  vfintle  4546  vfinncvntnn  4548  phiexg  4571  opexg  4587  proj1exg  4591  proj2exg  4592  setconslem5  4735  1stex  4739  swapex  4742  ssetex  4744  imaexg  4746  coexg  4749  siexg  4752  rnexg  5104  resexg  5116  ins2exg  5795  ins3exg  5796  mptexlem  5810  mpt2exlem  5811  cupex  5816  composeex  5820  addcfnex  5824  fnsex  5832  crossex  5850  domfnex  5870  ranfnex  5871  transex  5910  foundex  5914  ider  5943  ssetpov  5944  eqer  5961  ener  6039  enmap2lem1  6063  enmap1lem1  6069  enpw  6087  ncsex  6111  ncpw1c  6154  1p1e2c  6155  2p1e3c  6156  ce0addcnnul  6179  ce2  6192  ce2nc1  6193  lecncvg  6199  tcncv  6226  tcfnex  6244  ncvsq  6256  vvsqenvv  6257  csucex  6259  addccan2nclem2  6264  nmembers1lem1  6268  nncdiv3lem2  6276  nchoicelem11  6299  nchoicelem19  6307  fnfreclem1  6317