Theorem 0ex 5245

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 5244. (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 5244	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4300	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1849	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3455	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2111  Vcvv 3436  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-nul 4284

This theorem is referenced by:  al0ssb  5246  sseliALT  5247  csbexg  5248  unisn2  5250  class2set  5293  0elpw  5294  0nep0  5296  unidif0  5298  iin0  5300  notzfaus  5301  intv  5302  snexALT  5321  p0ex  5322  dtruALT  5326  zfpair  5359  snex  5374  opex  5404  opthwiener  5454  0sn0ep  5520  opthprc  5680  nrelv  5740  dmsnsnsn  6167  0elon  6361  nsuceq0  6391  snsn0non  6432  iotaex  6457  fun0  6546  fvrn0  6850  fprg  7088  ovima0  7525  onint0  7724  tfinds2  7794  finds  7826  finds2  7828  xpexr  7848  soex  7851  supp0  8095  fvn0elsupp  8110  fvn0elsuppb  8111  brtpos0  8163  reldmtpos  8164  tfrlem16  8312  tz7.44-1  8325  seqomlem1  8369  1n0  8403  nlim1  8404  nlim2  8405  el1o  8410  om0  8432  mapdm0  8766  fsetexb  8788  0map0sn0  8809  ixpexg  8846  0elixp  8853  en0  8940  en0ALT  8941  en0r  8942  ensn1  8943  en1  8946  2dom  8952  map1  8962  enpr2d  8970  xp1en  8976  endisj  8977  pw2eng  8996  0domg  9017  map2xp  9060  limensuci  9066  snnen2o  9129  0sdom1dom  9130  rex2dom  9137  1sdom2dom  9138  unxpdom2  9144  sucxpdom  9145  isinf  9149  ac6sfi  9168  fodomfi  9196  fodomfiOLD  9214  0fsupp  9274  fi0  9304  oiexg  9421  brwdom  9453  brwdom2  9459  inf3lemb  9515  infeq5i  9526  dfom3  9537  cantnfvalf  9555  cantnfval2  9559  cantnfle  9561  cantnflt  9562  cantnff  9564  cantnf0  9565  cantnfp1lem1  9568  cantnfp1lem3  9570  cantnfp1  9571  cantnflem1a  9575  cantnflem1d  9578  cantnflem1  9579  cantnf  9583  cnfcomlem  9589  cnfcom  9590  cnfcom2lem  9591  cnfcom3  9594  ssttrcl  9605  ttrcltr  9606  ttrclss  9610  dmttrcl  9611  ttrclselem2  9616  tc0  9635  r10  9661  scottex  9778  djulcl  9803  djulf1o  9805  djuss  9813  djuun  9819  1stinl  9820  2ndinl  9821  infxpenlem  9904  fseqenlem1  9915  undjudom  10059  endjudisj  10060  djuen  10061  dju1dif  10064  dju1p1e2  10065  dju0en  10067  djucomen  10069  djuassen  10070  xpdjuen  10071  mapdjuen  10072  djuxpdom  10077  djuinf  10080  infdju1  10081  djulepw  10084  pwsdompw  10094  pwdjudom  10106  ackbij1lem14  10123  ackbij2lem2  10130  ackbij2lem3  10131  cf0  10142  cfeq0  10147  cfsuc  10148  cflim2  10154  isfin5  10190  isfin4p1  10206  fin1a2lem11  10301  fin1a2lem12  10302  fin1a2lem13  10303  axcc2lem  10327  ac6num  10370  zornn0g  10396  ttukeylem3  10402  brdom3  10419  iundom2g  10431  cardeq0  10443  pwcfsdom  10474  axpowndlem3  10490  canthwe  10542  canthp1lem1  10543  pwxpndom2  10556  pwdjundom  10558  gchxpidm  10560  intwun  10626  0tsk  10646  grothomex  10720  indpi  10798  fzennn  13875  hash0  14274  hashen1  14277  hashmap  14342  hashbc  14360  hashf1  14364  hashge3el3dif  14394  ccat1st1st  14536  swrdval  14551  swrd00  14552  swrd0  14566  cshfn  14697  cshnz  14699  0csh0  14700  incexclem  15743  incexc  15744  rexpen  16137  sadcf  16364  sadc0  16365  sadcp1  16366  smupf  16389  smup0  16390  smupp1  16391  0ram  16932  ram0  16934  cshws0  17013  str0  17100  ress0  17154  0rest  17333  fnpr2ob  17462  xpsfrnel  17466  xpsle  17483  ismred2  17505  acsfn  17565  0cat  17595  ciclcl  17709  cicrcl  17710  cicer  17713  setcepi  17995  setc2obas  18001  setc2ohom  18002  cat1  18004  0pos  18227  join0  18309  meet0  18310  mgm0b  18565  gsum0  18592  sgrp0b  18636  efmnd0nmnd  18798  pwmnd  18845  mulgfval  18982  ga0  19211  psgn0fv0  19424  pmtrsn  19432  oppglsm  19555  efgi0  19633  vrgpf  19681  vrgpinv  19682  frgpuptinv  19684  frgpup2  19689  0frgp  19692  frgpnabllem1  19786  frgpnabllem2  19787  dprd0  19946  dmdprdpr  19964  dprdpr  19965  00lsp  20915  cnfldfun  21306  cnfldfunOLD  21319  frgpcyg  21511  frlmiscvec  21787  fvcoe1  22121  coe1f2  22123  coe1sfi  22127  coe1add  22179  coe1mul2lem1  22182  coe1mul2lem2  22183  coe1mul2  22184  ply1coe  22214  evls1rhmlem  22237  evl1sca  22250  evl1var  22252  pf1mpf  22268  pf1ind  22271  mat0dimscm  22385  mat0dimcrng  22386  mat0scmat  22454  mavmul0  22468  mavmul0g  22469  mvmumamul1  22470  mdet0pr  22508  mdet0f1o  22509  mdet0fv0  22510  mdetunilem9  22536  d0mat2pmat  22654  chpmat0d  22750  en1top  22900  en2top  22901  sn0topon  22914  indistopon  22917  indistps  22927  indistps2  22928  sn0cld  23006  indiscld  23007  neipeltop  23045  rest0  23085  restsn  23086  cmpfi  23324  refun0  23431  txindislem  23549  hmphindis  23713  xpstopnlem1  23725  xpstopnlem2  23727  ptcmpfi  23729  snfil  23780  fbasfip  23784  fgcl  23794  filconn  23799  fbasrn  23800  cfinfil  23809  csdfil  23810  supfil  23811  ufildr  23847  fin1aufil  23848  rnelfmlem  23868  fclsval  23924  tmdgsum  24011  tsmsfbas  24044  ust0  24136  ustn0  24137  0met  24282  xpsdsval  24297  minveclem3b  25356  tdeglem2  25994  deg1ldg  26025  deg1leb  26028  deg1val  26029  ulm0  26328  nosgnn0  27598  nodense  27632  nolt02o  27635  nogt01o  27636  nulsslt  27739  nulssgt  27740  bday1s  27776  made0  27819  precsexlem1  28146  precsexlem2  28147  uhgr0  29052  upgr0eop  29093  upgr0eopALT  29095  usgr0  29222  usgr0eop  29225  lfuhgr1v0e  29233  griedg0prc  29243  0grsubgr  29257  cplgr0  29404  0grrusgr  29559  clwwlk0on0  30070  0ewlk  30092  0wlkon  30098  0trlon  30102  0pthon  30105  0pthonv  30107  0conngr  30170  konigsberglem1  30230  konigsberglem2  30231  konigsberglem3  30232  wlkl0  30345  disjdifprg  32553  disjun0  32573  of0r  32658  fpwrelmapffslem  32713  f1ocnt  32780  resvsca  33295  1arithidom  33500  locfinref  33852  zarcmplem  33892  esumnul  34059  esumrnmpt2  34079  prsiga  34142  ldsysgenld  34171  ldgenpisyslem1  34174  oms0  34308  carsggect  34329  eulerpartgbij  34383  eulerpartlemmf  34386  repr0  34622  breprexp  34644  bnj941  34782  bnj97  34876  bnj149  34885  bnj150  34886  bnj944  34948  fineqvac  35137  fineqvnttrclse  35142  wevgblacfn  35151  derang0  35211  indispconn  35276  goeleq12bg  35391  satf0  35414  satf0op  35419  fmla0  35424  fmla0xp  35425  fmlasuc0  35426  fmlafvel  35427  fmlasuc  35428  fmlaomn0  35432  fmla0disjsuc  35440  satfdmfmla  35442  satfv0fvfmla0  35455  sate0  35457  sate0fv0  35459  sategoelfvb  35461  ex-sategoelel  35463  prv0  35472  prv1n  35473  rdgprc  35834  dfrdg3  35836  fullfunfnv  35986  fullfunfv  35987  rank0  36210  ssoninhaus  36488  onint1  36489  bj-0nel1  36993  bj-xpnzex  36999  bj-eltag  37017  bj-0eltag  37018  bj-tagss  37020  bj-pr1val  37044  bj-snex  37075  bj-snfromadj  37084  bj-nuliota  37097  bj-nuliotaALT  37098  bj-rdg0gALT  37111  bj-rest10  37128  bj-rest10b  37129  bj-rest0  37133  rdgssun  37418  finxpreclem1  37429  finxpreclem2  37430  finxp0  37431  finxpreclem5  37435  poimirlem28  37694  heibor1lem  37855  heiborlem6  37862  reheibor  37885  n0elqs  38366  sticksstones11  42195  mzpcompact2lem  42790  wopprc  43069  pw2f1ocnv  43076  pwslnmlem0  43130  pwfi2f1o  43135  2omomeqom  43342  cantnfub  43360  cantnfresb  43363  omcl3g  43373  nadd1suc  43431  naddwordnexlem4  43440  nla0002  43463  nla0003  43464  nla0001  43465  clsk1indlem0  44080  clsk1indlem4  44083  clsk1indlem1  44084  mnupwd  44306  mnuprdlem1  44311  mnuprdlem2  44312  mnuprdlem3  44313  mnurnd  44322  permaxnul  45047  permaxinf2lem  45051  nregmodelf1o  45054  nregmodellem  45055  nregmodel  45056  fnchoice  45072  eliuniincex  45152  limsup0  45738  0cnv  45786  liminf0  45837  0cnf  45921  dvnprodlem3  45992  qndenserrnbl  46339  prsal  46362  intsal  46374  sge00  46420  sge0sn  46423  nnfoctbdjlem  46499  isomenndlem  46574  hoiqssbl  46669  ovnsubadd2lem  46689  iota0def  47075  aiota0def  47133  afv0fv0  47186  0nelsetpreimafv  47427  lincval0  48453  lco0  48465  linds0  48503  0aryfvalel  48672  0aryfvalelfv  48673  1aryenef  48683  2aryenef  48694  mof0  48875  dftpos5  48911  dftpos6  48912  relcic  49083  discsubclem  49101  discsubc  49102  iinfconstbas  49104  nelsubclem  49105  0funcg  49123  0func  49125  0funcALT  49126  oppffn  49162  oppfvalg  49164  fucofvalne  49363  0thinc  49497  setc2othin  49504  setc1ohomfval  49531  setc1ocofval  49532  isinito2lem  49536  prstcthin  49599  setc1onsubc  49640  initocmd  49707  termolmd  49708  bnd2d  49719