Theorem 0ex 5234

Description: The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 5233. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Assertion

Ref	Expression
0ex	⊢ ∅ ∈ V

Proof of Theorem 0ex

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-nul 5233	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4280	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1846	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3450	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2101  Vcvv 3434  ∅c0 4259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704  ax-nul 5233

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3436  df-dif 3892  df-nul 4260

This theorem is referenced by:  al0ssb  5235  sseliALT  5236  csbexg  5237  unisn2  5239  class2set  5279  0elpw  5281  0nep0  5283  unidif0  5285  iin0  5287  notzfaus  5288  intv  5289  snexALT  5309  p0ex  5310  dtruALT  5314  zfpair  5347  snex  5357  opex  5382  opthwiener  5431  0sn0ep  5501  opthprc  5653  nrelv  5713  dmsnsnsn  6127  0elon  6323  nsuceq0  6352  snsn0non  6393  iotaex  6420  iotaexOLD  6427  fun0  6516  fvrn0  6822  fvssunirn  6823  fprg  7047  ovima0  7471  onint0  7661  tfinds2  7730  finds  7765  finds2  7767  xpexr  7785  soex  7788  supp0  8002  fvn0elsupp  8016  fvn0elsuppb  8017  brtpos0  8069  reldmtpos  8070  tfrlem16  8244  tz7.44-1  8257  seqomlem1  8301  1n0  8338  nlim1  8339  nlim2  8340  el1o  8345  om0  8367  mapdm0  8650  fsetexb  8672  0map0sn0  8693  ixpexg  8730  0elixp  8737  en0  8827  en0OLD  8828  en0ALT  8829  en0r  8830  ensn1  8831  ensn1OLD  8832  en1  8835  en1OLD  8836  2dom  8844  map1  8854  xp1en  8869  endisj  8870  pw2eng  8890  0domg  8912  map2xp  8959  limensuci  8965  snnen2o  9045  0sdom1dom  9046  1sdom  9054  unxpdom2  9059  sucxpdom  9060  isinf  9064  ac6sfi  9086  fodomfi  9120  0fsupp  9178  fi0  9207  oiexg  9322  brwdom  9354  brwdom2  9360  inf3lemb  9411  infeq5i  9422  dfom3  9433  cantnfvalf  9451  cantnfval2  9455  cantnfle  9457  cantnflt  9458  cantnff  9460  cantnf0  9461  cantnfp1lem1  9464  cantnfp1lem3  9466  cantnfp1  9467  cantnflem1a  9471  cantnflem1d  9474  cantnflem1  9475  cantnf  9479  cnfcomlem  9485  cnfcom  9486  cnfcom2lem  9487  cnfcom3  9490  ssttrcl  9501  ttrcltr  9502  ttrclss  9506  dmttrcl  9507  ttrclselem2  9512  tc0  9533  r10  9554  scottex  9671  djulcl  9696  djulf1o  9698  djuss  9706  djuun  9712  1stinl  9713  2ndinl  9714  infxpenlem  9797  fseqenlem1  9808  undjudom  9951  endjudisj  9952  djuen  9953  dju1dif  9956  dju1p1e2  9957  dju0en  9959  djucomen  9961  djuassen  9962  xpdjuen  9963  mapdjuen  9964  djuxpdom  9969  djuinf  9972  infdju1  9973  djulepw  9976  pwsdompw  9988  pwdjudom  10000  ackbij1lem14  10017  ackbij2lem2  10024  ackbij2lem3  10025  cf0  10035  cfeq0  10040  cfsuc  10041  cflim2  10047  isfin5  10083  isfin4p1  10099  fin1a2lem11  10194  fin1a2lem12  10195  fin1a2lem13  10196  axcc2lem  10220  ac6num  10263  zornn0g  10289  ttukeylem3  10295  brdom3  10312  iundom2g  10324  cardeq0  10336  pwcfsdom  10367  axpowndlem3  10383  canthwe  10435  canthp1lem1  10436  pwxpndom2  10449  pwdjundom  10451  gchxpidm  10453  intwun  10519  0tsk  10539  grothomex  10613  indpi  10691  fzennn  13716  hash0  14110  hashen1  14113  hashmap  14178  hashbc  14193  hashf1  14199  hashge3el3dif  14228  ccat1st1st  14363  swrdval  14384  swrd00  14385  swrd0  14399  cshfn  14531  cshnz  14533  0csh0  14534  incexclem  15576  incexc  15577  rexpen  15965  sadcf  16188  sadc0  16189  sadcp1  16190  smupf  16213  smup0  16214  smupp1  16215  0ram  16749  ram0  16751  cshws0  16831  str0  16918  ressbasOLD  16976  ress0  16981  0rest  17168  fnpr2ob  17297  xpsfrnel  17301  xpsle  17318  ismred2  17340  acsfn  17396  0cat  17426  ciclcl  17542  cicrcl  17543  cicer  17546  setcepi  17831  setc2obas  17837  setc2ohom  17838  cat1  17840  0pos  18067  0posOLD  18068  join0  18151  meet0  18152  mgm0b  18369  gsum0  18396  sgrp0b  18411  efmnd0nmnd  18557  pwmnd  18604  mulgfval  18730  ga0  18932  psgn0fv0  19147  pmtrsn  19155  oppglsm  19275  efgi0  19354  vrgpf  19402  vrgpinv  19403  frgpuptinv  19405  frgpup2  19410  0frgp  19413  frgpnabllem1  19502  frgpnabllem2  19503  dprd0  19662  dmdprdpr  19680  dprdpr  19681  00lsp  20271  cnfldfun  20637  frgpcyg  20809  frlmiscvec  21084  fvcoe1  21406  coe1f2  21408  coe1sfi  21412  coe1add  21463  coe1mul2lem1  21466  coe1mul2lem2  21467  coe1mul2  21468  ply1coe  21495  evls1rhmlem  21515  evl1sca  21528  evl1var  21530  pf1mpf  21546  pf1ind  21549  mat0dimscm  21646  mat0dimcrng  21647  mat0scmat  21715  mavmul0  21729  mavmul0g  21730  mvmumamul1  21731  mdet0pr  21769  mdet0f1o  21770  mdet0fv0  21771  mdetunilem9  21797  d0mat2pmat  21915  chpmat0d  22011  en1top  22162  en2top  22163  sn0topon  22176  indistopon  22179  indistps  22189  indistps2  22190  sn0cld  22269  indiscld  22270  neipeltop  22308  rest0  22348  restsn  22349  cmpfi  22587  refun0  22694  txindislem  22812  hmphindis  22976  xpstopnlem1  22988  xpstopnlem2  22990  ptcmpfi  22992  snfil  23043  fbasfip  23047  fgcl  23057  filconn  23062  fbasrn  23063  cfinfil  23072  csdfil  23073  supfil  23074  ufildr  23110  fin1aufil  23111  rnelfmlem  23131  fclsval  23187  tmdgsum  23274  tsmsfbas  23307  ust0  23399  ustn0  23400  0met  23547  xpsdsval  23562  minveclem3b  24620  tdeglem2  25254  deg1ldg  25285  deg1leb  25288  deg1val  25289  ulm0  25578  uhgr0  27471  upgr0eop  27512  upgr0eopALT  27514  usgr0  27638  usgr0eop  27641  lfuhgr1v0e  27649  griedg0prc  27659  0grsubgr  27673  cplgr0  27820  0grrusgr  27974  clwwlk0on0  28484  0ewlk  28506  0wlkon  28512  0trlon  28516  0pthon  28519  0pthonv  28521  0conngr  28584  konigsberglem1  28644  konigsberglem2  28645  konigsberglem3  28646  wlkl0  28759  disjdifprg  30942  disjun0  30962  fpwrelmapffslem  31095  f1ocnt  31151  resvsca  31557  locfinref  31819  zarcmplem  31859  esumnul  32044  esumrnmpt2  32064  prsiga  32127  ldsysgenld  32156  ldgenpisyslem1  32159  oms0  32292  carsggect  32313  eulerpartgbij  32367  eulerpartlemmf  32370  repr0  32619  breprexp  32641  bnj941  32780  bnj97  32874  bnj149  32883  bnj150  32884  bnj944  32946  fineqvac  33094  derang0  33159  indispconn  33224  goeleq12bg  33339  satf0  33362  satf0op  33367  fmla0  33372  fmla0xp  33373  fmlasuc0  33374  fmlafvel  33375  fmlasuc  33376  fmlaomn0  33380  fmla0disjsuc  33388  satfdmfmla  33390  satfv0fvfmla0  33403  sate0  33405  sate0fv0  33407  sategoelfvb  33409  ex-sategoelel  33411  prv0  33420  prv1n  33421  rdgprc  33798  dfrdg3  33800  nosgnn0  33889  nodense  33923  nolt02o  33926  nogt01o  33927  nulsslt  34019  nulssgt  34020  bday1s  34053  made0  34085  fullfunfnv  34276  fullfunfv  34277  rank0  34500  ssoninhaus  34665  onint1  34666  bj-0nel1  35171  bj-xpnzex  35177  bj-eltag  35195  bj-0eltag  35196  bj-tagss  35198  bj-pr1val  35222  bj-nuliota  35256  bj-nuliotaALT  35257  bj-rdg0gALT  35270  bj-rest10  35287  bj-rest10b  35288  bj-rest0  35292  rdgssun  35577  finxpreclem1  35588  finxpreclem2  35589  finxp0  35590  finxpreclem5  35594  poimirlem28  35833  heibor1lem  35995  heiborlem6  36002  reheibor  36025  n0elqs  36487  sticksstones11  40138  mzpcompact2lem  40596  wopprc  40876  pw2f1ocnv  40883  pwslnmlem0  40940  pwfi2f1o  40945  clsk1indlem0  41675  clsk1indlem4  41678  clsk1indlem1  41679  mnupwd  41909  mnuprdlem1  41914  mnuprdlem2  41915  mnuprdlem3  41916  mnurnd  41925  fnchoice  42596  eliuniincex  42683  limsup0  43270  0cnv  43318  liminf0  43369  0cnf  43453  dvnprodlem3  43524  qndenserrnbl  43871  prsal  43894  intsal  43904  sge00  43950  sge0sn  43953  nnfoctbdjlem  44029  isomenndlem  44104  hoiqssbl  44199  ovnsubadd2lem  44219  iota0def  44572  aiota0def  44628  afv0fv0  44681  0nelsetpreimafv  44882  lincval0  45796  lco0  45808  linds0  45846  0aryfvalel  46020  0aryfvalelfv  46021  1aryenef  46031  2aryenef  46042  mof0  46205  0thinc  46372  setc2othin  46377  prstcthin  46397  bnd2d  46427  upwordnul  46555