Theorem 0ex 5254

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

Syntax hints:  ¬ wn 3  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141  Vcvv 3453  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905  df-nul 4284

This theorem is referenced by:  al0ssb  5255  sseliALT  5256  csbexg  5257  unisn2  5259  class2set  5308  0elpw  5309  0nep0  5311  unidif0  5313  unidif0OLD  5314  iin0  5316  notzfaus  5317  intv  5318  snexALT  5337  p0ex  5338  dtruALT  5342  zfpair  5375  snexOLD  5396  opexOLD  5429  opthwiener  5480  0sn0ep  5547  opthprc  5707  nrelv  5768  nrelvOLD  5769  dmsnsnsn  6202  0elon  6396  nsuceq0  6426  snsn0non  6467  iotaex  6492  fun0  6581  fvrn0  6890  fprg  7133  ovima0  7570  onint0  7769  tfinds2  7839  finds  7872  finds2  7874  xpexr  7894  soex  7897  supp0  8139  fvn0elsupp  8154  fvn0elsuppb  8155  brtpos0  8207  reldmtpos  8208  tfrlem16  8358  tz7.44-1  8371  seqomlem1  8415  1n0OLD  8451  nlim1  8452  nlim2  8453  el1o  8458  om0  8480  mapdm0  8817  fsetexb  8839  0map0sn0  8861  ixpexg  8898  0elixp  8905  en0  8993  en0ALT  8994  en0r  8995  ensn1  8996  en1  8999  2dom  9005  map1  9015  enpr2d  9023  xp1en  9029  endisj  9030  pw2eng  9049  0domg  9070  map2xp  9113  limensuci  9119  snnen2o  9183  0sdom1dom  9184  rex2dom  9191  1sdom2dom  9192  unxpdom2  9198  sucxpdom  9199  isinf  9203  ac6sfi  9222  fodomfi  9250  0fsupp  9330  fi0  9360  oiexg  9477  brwdom  9509  brwdom2  9515  inf3lemb  9574  infeq5i  9585  dfom3  9596  cantnfvalf  9614  cantnfval2  9618  cantnfle  9620  cantnflt  9621  cantnff  9623  cantnf0  9624  cantnfp1lem1  9627  cantnfp1lem3  9629  cantnfp1  9630  cantnflem1a  9634  cantnflem1d  9637  cantnflem1  9638  cantnf  9642  cnfcomlem  9648  cnfcom  9649  cnfcom2lem  9650  cnfcom3  9653  ssttrcl  9664  ttrcltr  9665  ttrclss  9669  dmttrcl  9670  ttrclselem2  9675  tc0  9694  r10  9720  scottex  9837  djulcl  9862  djulf1o  9864  djuss  9872  djuun  9878  1stinl  9879  2ndinl  9880  infxpenlem  9963  fseqenlem1  9974  undjudom  10118  endjudisj  10119  djuen  10120  dju1dif  10123  dju1p1e2  10124  dju0en  10126  djucomen  10128  djuassen  10129  xpdjuen  10130  mapdjuen  10131  djuxpdom  10136  djuinf  10139  infdju1  10140  djulepw  10143  pwsdompw  10153  pwdjudom  10165  ackbij1lem14  10182  ackbij2lem2  10189  ackbij2lem3  10190  cf0  10201  cfeq0  10207  cfsuc  10208  cflim2  10214  isfin5  10250  isfin4p1  10266  fin1a2lem11  10361  fin1a2lem12  10362  fin1a2lem13  10363  axcc2lem  10387  ac6num  10430  zornn0g  10456  ttukeylem3  10462  brdom3  10479  iundom2g  10491  cardeq0  10503  pwcfsdom  10535  axpowndlem3  10551  canthwe  10603  canthp1lem1  10604  pwxpndom2  10617  pwdjundom  10619  gchxpidm  10621  intwun  10687  0tsk  10707  grothomex  10781  indpi  10859  fzennn  13975  hash0  14374  hashen1  14377  hashmap  14442  hashbc  14460  hashf1  14464  hashge3el3dif  14494  ccat1st1st  14636  swrdval  14651  swrd00  14652  swrd0  14666  cshfn  14797  cshnz  14799  0csh0  14800  incexclem  15857  incexc  15858  rexpen  16251  sadcf  16478  sadc0  16479  sadcp1  16480  smupf  16503  smup0  16504  smupp1  16505  0ram  17047  ram0  17049  cshws0  17128  str0  17216  ress0  17270  0rest  17449  fnpr2ob  17579  xpsfrnel  17583  xpsle  17600  ismred2  17622  acsfn  17682  0cat  17712  ciclcl  17826  cicrcl  17827  cicer  17830  setcepi  18112  setc2obas  18118  setc2ohom  18119  cat1  18121  0pos  18344  join0  18426  meet0  18427  mgm0b  18682  gsum0  18709  sgrp0b  18753  efmnd0nmnd  18915  pwmnd  18965  mulgfval  19102  ga0  19329  psgn0fv0  19542  pmtrsn  19550  oppglsm  19673  efgi0  19751  vrgpf  19799  vrgpinv  19800  frgpuptinv  19802  frgpup2  19807  0frgp  19810  frgpnabllem1  19904  frgpnabllem2  19905  dprd0  20064  dmdprdpr  20082  dprdpr  20083  00lsp  21036  cnfldfun  21426  frgpcyg  21613  frlmiscvec  21889  fvcoe1  22257  coe1f2  22259  coe1sfi  22263  coe1add  22315  coe1mul2lem1  22318  coe1mul2lem2  22319  coe1mul2  22320  ply1coe  22349  evls1rhmlem  22372  evl1sca  22385  evl1var  22387  pf1mpf  22403  pf1ind  22406  mat0dimscm  22517  mat0dimcrng  22518  mat0scmat  22586  mavmul0  22600  mavmul0g  22601  mvmumamul1  22602  mdet0pr  22640  mdet0f1o  22641  mdet0fv0  22642  mdetunilem9  22668  d0mat2pmat  22786  chpmat0d  22882  en1top  23032  en2top  23033  sn0topon  23046  indistopon  23049  indistps  23059  indistps2  23060  sn0cld  23138  indiscld  23139  neipeltop  23177  rest0  23217  restsn  23218  cmpfi  23456  refun0  23563  txindislem  23681  hmphindis  23845  xpstopnlem1  23857  xpstopnlem2  23859  ptcmpfi  23861  snfil  23912  fbasfip  23916  fgcl  23926  filconn  23931  fbasrn  23932  cfinfil  23941  csdfil  23942  supfil  23943  ufildr  23979  fin1aufil  23980  rnelfmlem  24000  fclsval  24056  tmdgsum  24143  tsmsfbas  24176  ust0  24268  ustn0  24269  0met  24414  xpsdsval  24429  minveclem3b  25478  tdeglem2  26109  deg1ldg  26140  deg1leb  26143  deg1val  26144  ulm0  26442  nosgnn0  27710  nodense  27744  nolt02o  27747  nogt01o  27748  nulslts  27856  nulsgts  27857  bday1  27895  made0  27944  precsexlem1  28288  precsexlem2  28289  uhgr0  29231  upgr0eop  29272  upgr0eopALT  29274  usgr0  29401  usgr0eop  29404  lfuhgr1v0e  29412  griedg0prc  29422  0grsubgr  29436  cplgr0  29583  0grrusgr  29737  clwwlk0on0  30251  0ewlk  30273  0wlkon  30279  0trlon  30283  0pthon  30286  0pthonv  30288  0conngr  30351  konigsberglem1  30411  konigsberglem2  30412  konigsberglem3  30413  wlkl0  30526  disjdifprg  32735  disjun0  32755  of0r  32842  fpwrelmapffslem  32895  f1ocnt  32963  resvsca  33479  1arithidom  33694  0mplrim  33772  selvply1rhmlema  33776  selvply1rhmlemb  33777  selvply1rhmlem1  33778  selvply1rhm0  33784  mplidomlem  33785  vieta  33838  locfinref  34099  zarcmplem  34139  esumnul  34306  esumrnmpt2  34326  prsiga  34389  ldsysgenld  34418  ldgenpisyslem1  34421  oms0  34555  carsggect  34576  eulerpartgbij  34630  eulerpartlemmf  34633  repr0  34866  breprexp  34888  bnj941  35029  bnj97  35122  bnj149  35131  bnj150  35132  bnj944  35194  fineqvac  35373  fineqvnttrclse  35381  wevgblacfn  35415  derang0  35480  indispconn  35545  goeleq12bg  35660  satf0  35683  satf0op  35688  fmla0  35693  fmla0xp  35694  fmlasuc0  35695  fmlafvel  35696  fmlasuc  35697  fmlaomn0  35701  fmla0disjsuc  35709  satfdmfmla  35711  satfv0fvfmla0  35724  sate0  35726  sate0fv0  35728  sategoelfvb  35730  ex-sategoelel  35732  prv0  35741  prv1n  35742  rdgprc  36103  dfrdg3  36105  fullfunfnv  36257  fullfunfv  36258  rank0  36481  ssoninhaus  36769  onint1  36770  mh-infprim2bi  36868  bj-0nel1  37399  bj-xpnzex  37405  bj-eltag  37423  bj-0eltag  37424  bj-tagss  37426  bj-pr1val  37450  bj-snex  37481  bj-snfromadj  37490  bj-nuliota  37503  bj-nuliotaALT  37504  bj-rdg0gALT  37517  bj-rest10  37539  bj-rest10b  37540  bj-rest0  37544  rdgssun  37833  finxpreclem1  37844  finxpreclem2  37845  finxp0  37846  finxpreclem5  37850  poimirlem28  38108  heibor1lem  38269  heiborlem6  38276  reheibor  38299  n0elqs  38792  sticksstones11  42734  mzpcompact2lem  43293  wopprc  43568  pw2f1ocnv  43575  pwslnmlem0  43629  pwfi2f1o  43634  2omomeqom  43841  cantnfub  43859  cantnfresb  43862  omcl3g  43872  nadd1suc  43930  naddwordnexlem4  43939  nla0002  43961  nla0003  43962  nla0001  43963  clsk1indlem0  44578  clsk1indlem4  44581  clsk1indlem1  44582  mnupwd  44804  mnuprdlem1  44809  mnuprdlem2  44810  mnuprdlem3  44811  mnurnd  44820  permaxnul  45545  permaxinf2lem  45549  nregmodelf1o  45552  nregmodellem  45553  nregmodel  45554  fnchoice  45570  eliuniincex  45648  limsup0  46229  0cnv  46277  liminf0  46328  0cnf  46412  dvnprodlem3  46483  qndenserrnbl  46830  prsal  46853  intsal  46865  sge00  46911  sge0sn  46914  nnfoctbdjlem  46990  isomenndlem  47065  hoiqssbl  47160  ovnsubadd2lem  47180  iota0def  47593  aiota0def  47651  afv0fv0  47704  0nelsetpreimafv  47957  lincval0  48998  lco0  49010  linds0  49048  0aryfvalel  49217  0aryfvalelfv  49218  1aryenef  49228  2aryenef  49239  mof0  49420  dftpos5  49456  dftpos6  49457  relcic  49627  discsubclem  49645  discsubc  49646  iinfconstbas  49648  nelsubclem  49649  0funcg  49667  0func  49669  0funcALT  49670  oppffn  49706  oppfvalg  49708  fucofvalne  49907  0thinc  50041  setc2othin  50048  setc1ohomfval  50075  setc1ocofval  50076  isinito2lem  50080  prstcthin  50143  setc1onsubc  50184  initocmd  50251  termolmd  50252  bnd2d  50263