Theorem 0ex 5260

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047  df-nul 4279

This theorem is used by:  al0ssb  5261  sseliALT  5262  csbexg  5263  unisn2  5265  class2set  5315  0elpw  5316  0nep0  5318  unidif0  5320  unidif0OLD  5321  iin0  5323  notsep  5324  intv  5325  snexALT  5344  p0ex  5345  dtruALT  5349  zfpair  5382  snexOLD  5399  opexOLD  5432  opthwiener  5486  0sn0ep  5554  opthprc  5714  nrelv  5776  nrelvOLD  5777  dmsnsnsn  6221  0elon  6418  nsuceq0  6448  snsn0non  6489  iotaex  6514  fun0  6606  fvrn0  6914  fprg  7160  ovima0  7601  onint0  7806  tfinds2  7876  finds  7909  finds2  7911  xpexr  7931  soex  7934  supp0  8186  fvn0elsupp  8201  fvn0elsuppb  8202  brtpos0  8254  reldmtpos  8255  tfrlem16  8405  tz7.44-1  8418  seqomlem1  8464  1n0OLD  8500  nlim1  8501  nlim2  8502  el1o  8507  om0  8529  mapdm0  8866  fsetexb  8890  0map0sn0  8917  ixpexg  8954  0elixp  8961  en0  9049  en0ALT  9050  en0r  9051  ensn1  9052  en1  9055  2dom  9062  map1  9072  enpr2d  9080  xp1en  9086  endisj  9087  pw2eng  9106  0domg  9127  map2xp  9170  limensuci  9176  snnen2o  9240  0sdom1dom  9241  rex2dom  9248  1sdom2dom  9249  unxpdom2  9255  sucxpdom  9256  isinf  9260  ac6sfi  9279  fodomfi  9308  0fsupp  9386  fi0  9416  oiexg  9533  brwdom  9565  brwdom2  9571  inf3lemb  9630  infeq5i  9641  dfom3  9652  cantnfvalf  9670  cantnfval2  9674  cantnfle  9676  cantnflt  9677  cantnff  9679  cantnf0  9680  cantnfp1lem1  9683  cantnfp1lem3  9685  cantnfp1  9686  cantnflem1a  9690  cantnflem1d  9693  cantnflem1  9694  cantnf  9698  cnfcomlem  9704  cnfcom  9705  cnfcom2lem  9706  cnfcom3  9709  ssttrcl  9720  ttrcltr  9721  ttrclss  9725  dmttrcl  9726  ttrclselem2  9731  tc0  9750  r10  9779  scottex  9937  scottexOLD  9938  bnd2d  9972  djulcl  9995  djulf1o  9997  djuss  10005  djuun  10011  1stinl  10012  2ndinl  10013  infxpenlem  10096  fseqenlem1  10107  undjudom  10250  endjudisj  10251  djuen  10252  dju1dif  10255  dju1p1e2  10256  dju0en  10258  djucomen  10260  djuassen  10261  xpdjuen  10262  mapdjuen  10263  djuxpdom  10268  djuinf  10271  infdju1  10272  djulepw  10275  pwsdompw  10285  pwdjudom  10297  ackbij1lem14  10314  ackbij2lem2  10321  ackbij2lem3  10322  cf0  10332  cfeq0  10338  cfsuc  10339  isfin5  10381  isfin4p1  10397  fin1a2lem11  10492  fin1a2lem12  10493  fin1a2lem13  10494  axcc2lem  10518  ac6num  10561  zornn0g  10587  ttukeylem3  10593  brdom3  10611  iundom2g  10628  cardeq0  10640  pwcfsdom  10672  axpowndlem3  10688  canthwe  10740  canthp1lem1  10741  pwxpndom2  10754  pwdjundom  10756  gchxpidm  10758  intwun  10824  0tsk  10844  grothomex  10918  indpi  10996  fzennn  14115  hash0  14515  hashen1  14518  hashmap  14584  hashbc  14602  hashf1  14606  hashge3el3dif  14636  ccat1st1st  14781  swrdval  14796  swrd00  14797  swrd0  14813  cshfn  14946  cshnz  14948  0csh0  14949  incexclem  16011  incexc  16012  rexpen  16402  sadcf  16629  sadc0  16630  sadcp1  16631  smupf  16654  smup0  16655  smupp1  16656  0ram  17204  ram0  17206  cshws0  17285  str0  17373  ress0  17427  0rest  17606  fnpr2ob  17736  xpsfrnel  17740  xpsle  17757  ismred2  17779  acsfn  17839  0cat  17869  ciclcl  17983  cicrcl  17984  cicer  17987  setcepi  18269  setc2obas  18275  setc2ohom  18276  cat1  18278  0pos  18501  join0  18583  meet0  18584  mgm0b  18841  gsum0  18879  sgrp0b  18923  efmnd0nmnd  19092  degenmgmopdm  19140  degenmgmnfn  19142  degenmgm  19143  degenmgm2  19146  pwmnd  19149  mulgfval  19285  ga0  19518  psgn0fv0  19731  pmtrsn  19739  oppglsm  19862  efgi0  19940  vrgpf  19988  vrgpinv  19989  frgpuptinv  19991  frgpup2  19996  0frgp  19999  frgpnabllem1  20093  frgpnabllem2  20094  dprd0  20253  dmdprdpr  20271  dprdpr  20272  00lsp  21262  cnfldfun  21698  frgpcyg  21885  frlmiscvec  22161  fvcoe1  22531  coe1f2  22533  coe1sfi  22537  coe1add  22589  coe1mul2lem1  22592  coe1mul2lem2  22593  coe1mul2  22594  ply1coe  22622  evls1rhmlem  22645  evl1sca  22658  evl1var  22660  pf1mpf  22676  pf1ind  22679  mat0dimscm  22790  mat0dimcrng  22791  mat0scmat  22859  mavmul0  22873  mavmul0g  22874  mvmumamul1  22875  mdet0pr  22913  mdet0f1o  22914  mdet0fv0  22915  mdetunilem9  22941  d0mat2pmat  23062  chpmat0d  23158  en1top  23308  en2top  23309  sn0topon  23322  indistopon  23325  indistps  23335  indistps2  23336  sn0cld  23414  indiscld  23415  neipeltop  23453  rest0  23493  restsn  23494  cmpfi  23732  refun0  23840  txindislem  23958  hmphindis  24122  xpstopnlem1  24134  xpstopnlem2  24136  ptcmpfi  24138  snfil  24189  fbasfip  24193  fgcl  24203  filconn  24208  fbasrn  24209  cfinfil  24218  csdfil  24219  supfil  24220  ufildr  24256  fin1aufil  24257  rnelfmlem  24277  fclsval  24333  tmdgsum  24420  tsmsfbas  24453  ust0  24545  ustn0  24546  0met  24691  xpsdsval  24706  minveclem3b  25755  tdeglem2  26385  deg1ldg  26416  deg1leb  26419  deg1val  26420  ulm0  26724  nosgnn0  28021  nodense  28055  nolt02o  28058  nogt01o  28059  nulslts  28167  nulsgts  28168  bday1  28206  made0  28255  precsexlem1  28599  precsexlem2  28600  uhgr0  29657  upgr0eop  29698  upgr0eopALT  29700  usgr0  29830  usgr0eop  29833  lfuhgr1v0e  29841  griedg0prc  29851  0grsubgr  29865  cplgr0  30012  0grrusgr  30166  clwwlk0on0  30689  0ewlk  30711  0wlkon  30717  0trlon  30721  0pthon  30724  0pthonv  30726  0conngr  30799  konigsberglem1  30859  konigsberglem2  30860  konigsberglem3  30861  wlkl0  30974  disjdifprg  33217  disjun0  33237  of0r  33321  fpwrelmapffslem  33371  f1ocnt  33439  resvsca  33940  1arithidom  34116  0mplrim  34193  selvply1rhmlema  34197  selvply1rhmlemb  34198  selvply1rhmlem1  34199  selvply1rhm0  34205  mplidomlem  34206  vieta  34259  locfinref  34520  zarcmplem  34560  esumnul  34727  esumrnmpt2  34747  prsiga  34810  ldsysgenld  34840  ldgenpisyslem1  34843  oms0  34976  carsggect  34997  eulerpartgbij  35051  eulerpartlemmf  35054  repr0  35287  breprexp  35309  bnj941  35450  bnj97  35543  bnj149  35552  bnj150  35553  bnj944  35615  fineqvac  35841  fineqvnttrclse  35849  kard0  35879  kard0b  35884  wevgblacfn  35959  derang0  36021  indispconn  36086  goeleq12bg  36201  satf0  36224  satf0op  36229  fmla0  36234  fmla0xp  36235  fmlasuc0  36236  fmlafvel  36237  fmlasuc  36238  fmlaomn0  36242  fmla0disjsuc  36250  satfdmfmla  36252  satfv0fvfmla0  36265  sate0  36267  sate0fv0  36269  sategoelfvb  36271  ex-sategoelel  36273  prv0  36282  prv1n  36283  rdgprc  36649  dfrdg3  36651  fullfunfnv  36803  fullfunfv  36804  rank0  37024  nmulrid  37039  ssoninhaus  37329  onint1  37330  mh-infprim2bi  37428  bj-0nel1  37959  bj-xpnzex  37965  bj-eltag  37983  bj-0eltag  37984  bj-tagss  37986  bj-pr1val  38010  bj-snex  38041  bj-snfromadj  38050  bj-nuliota  38065  bj-nuliotaALT  38066  bj-rdg0gALT  38079  bj-rest10  38102  bj-rest10b  38103  bj-rest0  38107  bj-pr0moore  38130  rdgssun  38395  finxpreclem1  38406  finxpreclem2  38407  finxp0  38408  finxpreclem5  38412  poimirlem28  38660  varprop  38736  heibor1lem  38837  heiborlem6  38844  reheibor  38867  n0elqs  39358  sticksstones11  43300  mzpcompact2lem  43856  wopprc  44131  pw2f1ocnv  44138  pwslnmlem0  44187  pwfi2f1o  44192  2omomeqom  44399  cantnfub  44417  cantnfresb  44420  omcl3g  44430  nadd1suc  44488  naddwordnexlem4  44497  nla0002  44519  nla0003  44520  nla0001  44521  clsk1indlem0  45135  clsk1indlem4  45138  clsk1indlem1  45139  mnupwd  45345  mnuprdlem1  45350  mnuprdlem2  45351  mnuprdlem3  45352  mnurnd  45361  permaxnul  46092  permaxinf2lem  46096  nregmodelf1o  46099  nregmodellem  46100  nregmodel  46101  fnchoice  46140  eliuniincex  46218  limsup0  46798  0cnv  46846  liminf0  46897  0cnf  46981  dvnprodlem3  47052  qndenserrnbl  47399  prsal  47422  intsal  47434  sge00  47480  sge0sn  47483  nnfoctbdjlem  47559  isomenndlem  47634  hoiqssbl  47729  ovnsubadd2lem  47749  iota0def  48202  aiota0def  48260  afv0fv0  48313  0nelsetpreimafv  48566  lincval0  49621  lco0  49633  linds0  49671  0aryfvalel  49840  0aryfvalelfv  49841  1aryenef  49851  2aryenef  49862  mof0  50043  dftpos5  50081  dftpos6  50082  relcic  50253  discsubclem  50271  discsubc  50272  iinfconstbas  50274  nelsubclem  50275  0funcg  50294  0func  50296  0funcALT  50297  oppffn  50334  oppfvalg  50336  fucofvalne  50541  0thinc  50688  setc2othin  50695  setc1ohomfval  50722  setc1ocofval  50723  isinito2lem  50727  prstcthin  50793  setc1onsubc  50834  parhomval  50837  parswapval  50870  parswapprop  50871  par2hom  50873  par2diag  50874  fuconuniqlem  50875  fuconuniqvalslem  50877  initocmd  50946  termolmd  50947