Theorem vvex 4110

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 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

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