Theorem 0ex 5261

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

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

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 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-nul 4280

This theorem is used by:  al0ssb  5262  sseliALT  5263  csbexg  5264  unisn2  5266  class2set  5316  0elpw  5317  0nep0  5319  unidif0  5321  unidif0OLD  5322  iin0  5324  notsep  5325  intv  5326  snexALT  5345  p0ex  5346  dtruALT  5350  zfpair  5383  snexOLD  5400  opexOLD  5433  opthwiener  5487  0sn0ep  5555  opthprc  5715  nrelv  5777  nrelvOLD  5778  dmsnsnsn  6220  0elon  6417  nsuceq0  6447  snsn0non  6488  iotaex  6513  fun0  6603  fvrn0  6911  fprg  7157  ovima0  7598  onint0  7803  tfinds2  7873  finds  7906  finds2  7908  xpexr  7928  soex  7931  supp0  8175  fvn0elsupp  8190  fvn0elsuppb  8191  brtpos0  8243  reldmtpos  8244  tfrlem16  8394  tz7.44-1  8407  seqomlem1  8453  1n0OLD  8489  nlim1  8490  nlim2  8491  el1o  8496  om0  8518  mapdm0  8855  fsetexb  8879  0map0sn0  8906  ixpexg  8943  0elixp  8950  en0  9038  en0ALT  9039  en0r  9040  ensn1  9041  en1  9044  2dom  9051  map1  9061  enpr2d  9069  xp1en  9075  endisj  9076  pw2eng  9095  0domg  9116  map2xp  9159  limensuci  9165  snnen2o  9229  0sdom1dom  9230  rex2dom  9237  1sdom2dom  9238  unxpdom2  9244  sucxpdom  9245  isinf  9249  ac6sfi  9268  fodomfi  9297  0fsupp  9375  fi0  9405  oiexg  9522  brwdom  9554  brwdom2  9560  inf3lemb  9619  infeq5i  9630  dfom3  9641  cantnfvalf  9659  cantnfval2  9663  cantnfle  9665  cantnflt  9666  cantnff  9668  cantnf0  9669  cantnfp1lem1  9672  cantnfp1lem3  9674  cantnfp1  9675  cantnflem1a  9679  cantnflem1d  9682  cantnflem1  9683  cantnf  9687  cnfcomlem  9693  cnfcom  9694  cnfcom2lem  9695  cnfcom3  9698  ssttrcl  9709  ttrcltr  9710  ttrclss  9714  dmttrcl  9715  ttrclselem2  9720  tc0  9739  r10  9768  scottex  9926  scottexOLD  9927  bnd2d  9961  djulcl  9984  djulf1o  9986  djuss  9994  djuun  10000  1stinl  10001  2ndinl  10002  infxpenlem  10085  fseqenlem1  10096  undjudom  10239  endjudisj  10240  djuen  10241  dju1dif  10244  dju1p1e2  10245  dju0en  10247  djucomen  10249  djuassen  10250  xpdjuen  10251  mapdjuen  10252  djuxpdom  10257  djuinf  10260  infdju1  10261  djulepw  10264  pwsdompw  10274  pwdjudom  10286  ackbij1lem14  10303  ackbij2lem2  10310  ackbij2lem3  10311  cf0  10321  cfeq0  10327  cfsuc  10328  cflim2  10334  isfin5  10370  isfin4p1  10386  fin1a2lem11  10481  fin1a2lem12  10482  fin1a2lem13  10483  axcc2lem  10507  ac6num  10550  zornn0g  10576  ttukeylem3  10582  brdom3  10600  iundom2g  10617  cardeq0  10629  pwcfsdom  10661  axpowndlem3  10677  canthwe  10729  canthp1lem1  10730  pwxpndom2  10743  pwdjundom  10745  gchxpidm  10747  intwun  10813  0tsk  10833  grothomex  10907  indpi  10985  fzennn  14104  hash0  14504  hashen1  14507  hashmap  14573  hashbc  14591  hashf1  14595  hashge3el3dif  14625  ccat1st1st  14769  swrdval  14784  swrd00  14785  swrd0  14801  cshfn  14934  cshnz  14936  0csh0  14937  incexclem  15998  incexc  15999  rexpen  16389  sadcf  16616  sadc0  16617  sadcp1  16618  smupf  16641  smup0  16642  smupp1  16643  0ram  17191  ram0  17193  cshws0  17272  str0  17360  ress0  17414  0rest  17593  fnpr2ob  17723  xpsfrnel  17727  xpsle  17744  ismred2  17766  acsfn  17826  0cat  17856  ciclcl  17970  cicrcl  17971  cicer  17974  setcepi  18256  setc2obas  18262  setc2ohom  18263  cat1  18265  0pos  18488  join0  18570  meet0  18571  mgm0b  18828  gsum0  18866  sgrp0b  18910  efmnd0nmnd  19079  degenmgmopdm  19127  degenmgmnfn  19129  degenmgm  19130  degenmgm2  19133  pwmnd  19136  mulgfval  19272  ga0  19505  psgn0fv0  19718  pmtrsn  19726  oppglsm  19849  efgi0  19927  vrgpf  19975  vrgpinv  19976  frgpuptinv  19978  frgpup2  19983  0frgp  19986  frgpnabllem1  20080  frgpnabllem2  20081  dprd0  20240  dmdprdpr  20258  dprdpr  20259  00lsp  21249  cnfldfun  21685  frgpcyg  21872  frlmiscvec  22148  fvcoe1  22518  coe1f2  22520  coe1sfi  22524  coe1add  22576  coe1mul2lem1  22579  coe1mul2lem2  22580  coe1mul2  22581  ply1coe  22609  evls1rhmlem  22632  evl1sca  22645  evl1var  22647  pf1mpf  22663  pf1ind  22666  mat0dimscm  22777  mat0dimcrng  22778  mat0scmat  22846  mavmul0  22860  mavmul0g  22861  mvmumamul1  22862  mdet0pr  22900  mdet0f1o  22901  mdet0fv0  22902  mdetunilem9  22928  d0mat2pmat  23049  chpmat0d  23145  en1top  23295  en2top  23296  sn0topon  23309  indistopon  23312  indistps  23322  indistps2  23323  sn0cld  23401  indiscld  23402  neipeltop  23440  rest0  23480  restsn  23481  cmpfi  23719  refun0  23827  txindislem  23945  hmphindis  24109  xpstopnlem1  24121  xpstopnlem2  24123  ptcmpfi  24125  snfil  24176  fbasfip  24180  fgcl  24190  filconn  24195  fbasrn  24196  cfinfil  24205  csdfil  24206  supfil  24207  ufildr  24243  fin1aufil  24244  rnelfmlem  24264  fclsval  24320  tmdgsum  24407  tsmsfbas  24440  ust0  24532  ustn0  24533  0met  24678  xpsdsval  24693  minveclem3b  25742  tdeglem2  26372  deg1ldg  26403  deg1leb  26406  deg1val  26407  ulm0  26711  nosgnn0  28008  nodense  28042  nolt02o  28045  nogt01o  28046  nulslts  28154  nulsgts  28155  bday1  28193  made0  28242  precsexlem1  28586  precsexlem2  28587  uhgr0  29644  upgr0eop  29685  upgr0eopALT  29687  usgr0  29817  usgr0eop  29820  lfuhgr1v0e  29828  griedg0prc  29838  0grsubgr  29852  cplgr0  29999  0grrusgr  30153  clwwlk0on0  30676  0ewlk  30698  0wlkon  30704  0trlon  30708  0pthon  30711  0pthonv  30713  0conngr  30786  konigsberglem1  30846  konigsberglem2  30847  konigsberglem3  30848  wlkl0  30961  disjdifprg  33162  disjun0  33182  of0r  33266  fpwrelmapffslem  33317  f1ocnt  33385  resvsca  33886  1arithidom  34062  0mplrim  34139  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem1  34145  selvply1rhm0  34151  mplidomlem  34152  vieta  34205  locfinref  34466  zarcmplem  34506  esumnul  34673  esumrnmpt2  34693  prsiga  34756  ldsysgenld  34786  ldgenpisyslem1  34789  oms0  34922  carsggect  34943  eulerpartgbij  34997  eulerpartlemmf  35000  repr0  35233  breprexp  35255  bnj941  35396  bnj97  35489  bnj149  35498  bnj150  35499  bnj944  35561  fineqvac  35767  fineqvnttrclse  35775  kard0  35805  kard0b  35810  wevgblacfn  35873  derang0  35913  indispconn  35978  goeleq12bg  36093  satf0  36116  satf0op  36121  fmla0  36126  fmla0xp  36127  fmlasuc0  36128  fmlafvel  36129  fmlasuc  36130  fmlaomn0  36134  fmla0disjsuc  36142  satfdmfmla  36144  satfv0fvfmla0  36157  sate0  36159  sate0fv0  36161  sategoelfvb  36163  ex-sategoelel  36165  prv0  36174  prv1n  36175  rdgprc  36536  dfrdg3  36538  fullfunfnv  36690  fullfunfv  36691  rank0  36911  nmulrid  36926  ssoninhaus  37216  onint1  37217  mh-infprim2bi  37315  bj-0nel1  37846  bj-xpnzex  37852  bj-eltag  37870  bj-0eltag  37871  bj-tagss  37873  bj-pr1val  37897  bj-snex  37928  bj-snfromadj  37937  bj-nuliota  37952  bj-nuliotaALT  37953  bj-rdg0gALT  37966  bj-rest10  37989  bj-rest10b  37990  bj-rest0  37994  rdgssun  38281  finxpreclem1  38292  finxpreclem2  38293  finxp0  38294  finxpreclem5  38298  poimirlem28  38546  varprop  38622  heibor1lem  38723  heiborlem6  38730  reheibor  38753  n0elqs  39244  sticksstones11  43186  mzpcompact2lem  43741  wopprc  44016  pw2f1ocnv  44023  pwslnmlem0  44077  pwfi2f1o  44082  2omomeqom  44289  cantnfub  44307  cantnfresb  44310  omcl3g  44320  nadd1suc  44378  naddwordnexlem4  44387  nla0002  44409  nla0003  44410  nla0001  44411  clsk1indlem0  45026  clsk1indlem4  45029  clsk1indlem1  45030  mnupwd  45236  mnuprdlem1  45241  mnuprdlem2  45242  mnuprdlem3  45243  mnurnd  45252  permaxnul  45976  permaxinf2lem  45980  nregmodelf1o  45983  nregmodellem  45984  nregmodel  45985  fnchoice  46015  eliuniincex  46093  limsup0  46673  0cnv  46721  liminf0  46772  0cnf  46856  dvnprodlem3  46927  qndenserrnbl  47274  prsal  47297  intsal  47309  sge00  47355  sge0sn  47358  nnfoctbdjlem  47434  isomenndlem  47509  hoiqssbl  47604  ovnsubadd2lem  47624  iota0def  48077  aiota0def  48135  afv0fv0  48188  0nelsetpreimafv  48441  lincval0  49496  lco0  49508  linds0  49546  0aryfvalel  49715  0aryfvalelfv  49716  1aryenef  49726  2aryenef  49737  mof0  49917  dftpos5  49951  dftpos6  49952  relcic  50122  discsubclem  50140  discsubc  50141  iinfconstbas  50143  nelsubclem  50144  0funcg  50162  0func  50164  0funcALT  50165  oppffn  50201  oppfvalg  50203  fucofvalne  50402  0thinc  50536  setc2othin  50543  setc1ohomfval  50570  setc1ocofval  50571  isinito2lem  50575  prstcthin  50638  setc1onsubc  50679  initocmd  50746  termolmd  50747