Theorem 0ex 5272

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 5271. (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 5271	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4304	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1881	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 234	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3476	1 ⊢ ∅ ∈ V

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3457  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-nul 4287

This theorem is used by:  al0ssb  5273  sseliALT  5274  csbexg  5275  unisn2  5277  class2set  5327  0elpw  5328  0nep0  5330  unidif0  5332  unidif0OLD  5333  iin0  5335  notsep  5336  intv  5337  snexALT  5356  p0ex  5357  dtruALT  5361  zfpair  5394  snexOLD  5415  opexOLD  5448  opthwiener  5499  0sn0ep  5567  opthprc  5727  nrelv  5788  nrelvOLD  5789  dmsnsnsn  6223  0elon  6420  nsuceq0  6450  snsn0non  6491  iotaex  6516  fun0  6605  fvrn0  6913  fprg  7156  ovima0  7595  onint0  7792  tfinds2  7862  finds  7895  finds2  7897  xpexr  7917  soex  7920  supp0  8163  fvn0elsupp  8178  fvn0elsuppb  8179  brtpos0  8231  reldmtpos  8232  tfrlem16  8382  tz7.44-1  8395  seqomlem1  8439  1n0OLD  8475  nlim1  8476  nlim2  8477  el1o  8482  om0  8504  mapdm0  8841  fsetexb  8863  0map0sn0  8885  ixpexg  8922  0elixp  8929  en0  9017  en0ALT  9018  en0r  9019  ensn1  9020  en1  9023  2dom  9030  map1  9040  enpr2d  9048  xp1en  9054  endisj  9055  pw2eng  9074  0domg  9095  map2xp  9138  limensuci  9144  snnen2o  9208  0sdom1dom  9209  rex2dom  9216  1sdom2dom  9217  unxpdom2  9223  sucxpdom  9224  isinf  9228  ac6sfi  9247  fodomfi  9275  0fsupp  9353  fi0  9383  oiexg  9500  brwdom  9532  brwdom2  9538  inf3lemb  9597  infeq5i  9608  dfom3  9619  cantnfvalf  9637  cantnfval2  9641  cantnfle  9643  cantnflt  9644  cantnff  9646  cantnf0  9647  cantnfp1lem1  9650  cantnfp1lem3  9652  cantnfp1  9653  cantnflem1a  9657  cantnflem1d  9660  cantnflem1  9661  cantnf  9665  cnfcomlem  9671  cnfcom  9672  cnfcom2lem  9673  cnfcom3  9676  ssttrcl  9687  ttrcltr  9688  ttrclss  9692  dmttrcl  9693  ttrclselem2  9698  tc0  9717  r10  9743  scottex  9865  scottexOLD  9866  djulcl  9908  djulf1o  9910  djuss  9918  djuun  9924  1stinl  9925  2ndinl  9926  infxpenlem  10009  fseqenlem1  10020  undjudom  10163  endjudisj  10164  djuen  10165  dju1dif  10168  dju1p1e2  10169  dju0en  10171  djucomen  10173  djuassen  10174  xpdjuen  10175  mapdjuen  10176  djuxpdom  10181  djuinf  10184  infdju1  10185  djulepw  10188  pwsdompw  10198  pwdjudom  10210  ackbij1lem14  10227  ackbij2lem2  10234  ackbij2lem3  10235  cf0  10245  cfeq0  10251  cfsuc  10252  cflim2  10258  isfin5  10294  isfin4p1  10310  fin1a2lem11  10405  fin1a2lem12  10406  fin1a2lem13  10407  axcc2lem  10431  ac6num  10474  zornn0g  10500  ttukeylem3  10506  brdom3  10523  iundom2g  10535  cardeq0  10547  pwcfsdom  10579  axpowndlem3  10595  canthwe  10647  canthp1lem1  10648  pwxpndom2  10661  pwdjundom  10663  gchxpidm  10665  intwun  10731  0tsk  10751  grothomex  10825  indpi  10903  fzennn  14017  hash0  14416  hashen1  14419  hashmap  14485  hashbc  14503  hashf1  14507  hashge3el3dif  14537  ccat1st1st  14681  swrdval  14696  swrd00  14697  swrd0  14713  cshfn  14846  cshnz  14848  0csh0  14849  incexclem  15908  incexc  15909  rexpen  16301  sadcf  16528  sadc0  16529  sadcp1  16530  smupf  16553  smup0  16554  smupp1  16555  0ram  17097  ram0  17099  cshws0  17178  str0  17266  ress0  17320  0rest  17499  fnpr2ob  17629  xpsfrnel  17633  xpsle  17650  ismred2  17672  acsfn  17732  0cat  17762  ciclcl  17876  cicrcl  17877  cicer  17880  setcepi  18162  setc2obas  18168  setc2ohom  18169  cat1  18171  0pos  18394  join0  18476  meet0  18477  mgm0b  18732  gsum0  18763  sgrp0b  18807  efmnd0nmnd  18972  pwmnd  19022  mulgfval  19158  ga0  19391  psgn0fv0  19604  pmtrsn  19612  oppglsm  19735  efgi0  19813  vrgpf  19861  vrgpinv  19862  frgpuptinv  19864  frgpup2  19869  0frgp  19872  frgpnabllem1  19966  frgpnabllem2  19967  dprd0  20126  dmdprdpr  20144  dprdpr  20145  00lsp  21131  cnfldfun  21565  frgpcyg  21752  frlmiscvec  22028  fvcoe1  22396  coe1f2  22398  coe1sfi  22402  coe1add  22454  coe1mul2lem1  22457  coe1mul2lem2  22458  coe1mul2  22459  ply1coe  22487  evls1rhmlem  22510  evl1sca  22523  evl1var  22525  pf1mpf  22541  pf1ind  22544  mat0dimscm  22655  mat0dimcrng  22656  mat0scmat  22724  mavmul0  22738  mavmul0g  22739  mvmumamul1  22740  mdet0pr  22778  mdet0f1o  22779  mdet0fv0  22780  mdetunilem9  22806  d0mat2pmat  22924  chpmat0d  23020  en1top  23170  en2top  23171  sn0topon  23184  indistopon  23187  indistps  23197  indistps2  23198  sn0cld  23276  indiscld  23277  neipeltop  23315  rest0  23355  restsn  23356  cmpfi  23594  refun0  23701  txindislem  23819  hmphindis  23983  xpstopnlem1  23995  xpstopnlem2  23997  ptcmpfi  23999  snfil  24050  fbasfip  24054  fgcl  24064  filconn  24069  fbasrn  24070  cfinfil  24079  csdfil  24080  supfil  24081  ufildr  24117  fin1aufil  24118  rnelfmlem  24138  fclsval  24194  tmdgsum  24281  tsmsfbas  24314  ust0  24406  ustn0  24407  0met  24552  xpsdsval  24567  minveclem3b  25616  tdeglem2  26247  deg1ldg  26278  deg1leb  26281  deg1val  26282  ulm0  26583  nosgnn0  27851  nodense  27885  nolt02o  27888  nogt01o  27889  nulslts  27997  nulsgts  27998  bday1  28036  made0  28085  precsexlem1  28429  precsexlem2  28430  uhgr0  29452  upgr0eop  29493  upgr0eopALT  29495  usgr0  29622  usgr0eop  29625  lfuhgr1v0e  29633  griedg0prc  29643  0grsubgr  29657  cplgr0  29804  0grrusgr  29958  clwwlk0on0  30472  0ewlk  30494  0wlkon  30500  0trlon  30504  0pthon  30507  0pthonv  30509  0conngr  30572  konigsberglem1  30632  konigsberglem2  30633  konigsberglem3  30634  wlkl0  30747  disjdifprg  32949  disjun0  32969  of0r  33053  fpwrelmapffslem  33106  f1ocnt  33174  resvsca  33675  1arithidom  33850  0mplrim  33927  selvply1rhmlema  33931  selvply1rhmlemb  33932  selvply1rhmlem1  33933  selvply1rhm0  33939  mplidomlem  33940  vieta  33993  locfinref  34254  zarcmplem  34294  esumnul  34461  esumrnmpt2  34481  prsiga  34544  ldsysgenld  34574  ldgenpisyslem1  34577  oms0  34711  carsggect  34732  eulerpartgbij  34786  eulerpartlemmf  34789  repr0  35022  breprexp  35044  bnj941  35185  bnj97  35278  bnj149  35287  bnj150  35288  bnj944  35350  fineqvac  35545  fineqvnttrclse  35553  kard0  35583  kard0b  35588  wevgblacfn  35611  derang0  35674  indispconn  35739  goeleq12bg  35854  satf0  35877  satf0op  35882  fmla0  35887  fmla0xp  35888  fmlasuc0  35889  fmlafvel  35890  fmlasuc  35891  fmlaomn0  35895  fmla0disjsuc  35903  satfdmfmla  35905  satfv0fvfmla0  35918  sate0  35920  sate0fv0  35922  sategoelfvb  35924  ex-sategoelel  35926  prv0  35935  prv1n  35936  rdgprc  36297  dfrdg3  36299  fullfunfnv  36451  fullfunfv  36452  rank0  36675  nmulrid  36702  ssoninhaus  36992  onint1  36993  mh-infprim2bi  37091  bj-0nel1  37622  bj-xpnzex  37628  bj-eltag  37646  bj-0eltag  37647  bj-tagss  37649  bj-pr1val  37673  bj-snex  37704  bj-snfromadj  37713  bj-nuliota  37726  bj-nuliotaALT  37727  bj-rdg0gALT  37740  bj-rest10  37763  bj-rest10b  37764  bj-rest0  37768  rdgssun  38057  finxpreclem1  38068  finxpreclem2  38069  finxp0  38070  finxpreclem5  38074  poimirlem28  38332  heibor1lem  38493  heiborlem6  38500  reheibor  38523  n0elqs  39014  sticksstones11  42956  mzpcompact2lem  43515  wopprc  43790  pw2f1ocnv  43797  pwslnmlem0  43851  pwfi2f1o  43856  2omomeqom  44063  cantnfub  44081  cantnfresb  44084  omcl3g  44094  nadd1suc  44152  naddwordnexlem4  44161  nla0002  44183  nla0003  44184  nla0001  44185  clsk1indlem0  44800  clsk1indlem4  44803  clsk1indlem1  44804  mnupwd  45010  mnuprdlem1  45015  mnuprdlem2  45016  mnuprdlem3  45017  mnurnd  45026  permaxnul  45750  permaxinf2lem  45754  nregmodelf1o  45757  nregmodellem  45758  nregmodel  45759  fnchoice  45782  eliuniincex  45860  limsup0  46441  0cnv  46489  liminf0  46540  0cnf  46624  dvnprodlem3  46695  qndenserrnbl  47042  prsal  47065  intsal  47077  sge00  47123  sge0sn  47126  nnfoctbdjlem  47202  isomenndlem  47277  hoiqssbl  47372  ovnsubadd2lem  47392  iota0def  47808  aiota0def  47866  afv0fv0  47919  0nelsetpreimafv  48172  lincval0  49228  lco0  49240  linds0  49278  0aryfvalel  49447  0aryfvalelfv  49448  1aryenef  49458  2aryenef  49469  mof0  49649  dftpos5  49685  dftpos6  49686  relcic  49856  discsubclem  49874  discsubc  49875  iinfconstbas  49877  nelsubclem  49878  0funcg  49896  0func  49898  0funcALT  49899  oppffn  49935  oppfvalg  49937  fucofvalne  50136  0thinc  50270  setc2othin  50277  setc1ohomfval  50304  setc1ocofval  50305  isinito2lem  50309  prstcthin  50372  setc1onsubc  50413  initocmd  50480  termolmd  50481  bnd2d  50492