Theorem 0ex 5277

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

Syntax hints:  ¬ wn 3  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-nul 4309

This theorem is referenced by:  al0ssb  5278  sseliALT  5279  csbexg  5280  unisn2  5282  class2set  5325  0elpw  5326  0nep0  5328  unidif0  5330  iin0  5332  notzfaus  5333  intv  5334  snexALT  5353  p0ex  5354  dtruALT  5358  zfpair  5391  snex  5406  opex  5439  opthwiener  5489  0sn0ep  5557  opthprc  5718  nrelv  5779  dmsnsnsn  6209  0elon  6407  nsuceq0  6436  snsn0non  6478  iotaex  6503  iotaexOLD  6510  fun0  6600  fvrn0  6905  fvssunirnOLD  6909  fprg  7144  ovima0  7584  onint0  7783  tfinds2  7857  finds  7890  finds2  7892  xpexr  7912  soex  7915  supp0  8162  fvn0elsupp  8177  fvn0elsuppb  8178  brtpos0  8230  reldmtpos  8231  tfrlem16  8405  tz7.44-1  8418  seqomlem1  8462  1n0  8498  nlim1  8499  nlim2  8500  el1o  8505  om0  8527  mapdm0  8854  fsetexb  8876  0map0sn0  8897  ixpexg  8934  0elixp  8941  en0  9030  en0ALT  9031  en0r  9032  ensn1  9033  en1  9036  2dom  9042  map1  9052  enpr2d  9061  xp1en  9069  endisj  9070  pw2eng  9090  0domg  9112  map2xp  9159  limensuci  9165  snnen2o  9243  0sdom1dom  9244  rex2dom  9252  1sdom2dom  9253  1sdomOLD  9255  unxpdom2  9260  sucxpdom  9261  isinf  9266  isinfOLD  9267  ac6sfi  9290  fodomfi  9320  fodomfiOLD  9340  0fsupp  9400  fi0  9430  oiexg  9547  brwdom  9579  brwdom2  9585  inf3lemb  9637  infeq5i  9648  dfom3  9659  cantnfvalf  9677  cantnfval2  9681  cantnfle  9683  cantnflt  9684  cantnff  9686  cantnf0  9687  cantnfp1lem1  9690  cantnfp1lem3  9692  cantnfp1  9693  cantnflem1a  9697  cantnflem1d  9700  cantnflem1  9701  cantnf  9705  cnfcomlem  9711  cnfcom  9712  cnfcom2lem  9713  cnfcom3  9716  ssttrcl  9727  ttrcltr  9728  ttrclss  9732  dmttrcl  9733  ttrclselem2  9738  tc0  9759  r10  9780  scottex  9897  djulcl  9922  djulf1o  9924  djuss  9932  djuun  9938  1stinl  9939  2ndinl  9940  infxpenlem  10025  fseqenlem1  10036  undjudom  10180  endjudisj  10181  djuen  10182  dju1dif  10185  dju1p1e2  10186  dju0en  10188  djucomen  10190  djuassen  10191  xpdjuen  10192  mapdjuen  10193  djuxpdom  10198  djuinf  10201  infdju1  10202  djulepw  10205  pwsdompw  10215  pwdjudom  10227  ackbij1lem14  10244  ackbij2lem2  10251  ackbij2lem3  10252  cf0  10263  cfeq0  10268  cfsuc  10269  cflim2  10275  isfin5  10311  isfin4p1  10327  fin1a2lem11  10422  fin1a2lem12  10423  fin1a2lem13  10424  axcc2lem  10448  ac6num  10491  zornn0g  10517  ttukeylem3  10523  brdom3  10540  iundom2g  10552  cardeq0  10564  pwcfsdom  10595  axpowndlem3  10611  canthwe  10663  canthp1lem1  10664  pwxpndom2  10677  pwdjundom  10679  gchxpidm  10681  intwun  10747  0tsk  10767  grothomex  10841  indpi  10919  fzennn  13984  hash0  14383  hashen1  14386  hashmap  14451  hashbc  14469  hashf1  14473  hashge3el3dif  14503  ccat1st1st  14644  swrdval  14659  swrd00  14660  swrd0  14674  cshfn  14806  cshnz  14808  0csh0  14809  incexclem  15850  incexc  15851  rexpen  16244  sadcf  16470  sadc0  16471  sadcp1  16472  smupf  16495  smup0  16496  smupp1  16497  0ram  17038  ram0  17040  cshws0  17119  str0  17206  ress0  17262  0rest  17441  fnpr2ob  17570  xpsfrnel  17574  xpsle  17591  ismred2  17613  acsfn  17669  0cat  17699  ciclcl  17813  cicrcl  17814  cicer  17817  setcepi  18099  setc2obas  18105  setc2ohom  18106  cat1  18108  0pos  18331  join0  18413  meet0  18414  mgm0b  18633  gsum0  18660  sgrp0b  18704  efmnd0nmnd  18866  pwmnd  18913  mulgfval  19050  ga0  19279  psgn0fv0  19490  pmtrsn  19498  oppglsm  19621  efgi0  19699  vrgpf  19747  vrgpinv  19748  frgpuptinv  19750  frgpup2  19755  0frgp  19758  frgpnabllem1  19852  frgpnabllem2  19853  dprd0  20012  dmdprdpr  20030  dprdpr  20031  00lsp  20936  cnfldfun  21327  cnfldfunOLD  21340  frgpcyg  21532  frlmiscvec  21807  fvcoe1  22141  coe1f2  22143  coe1sfi  22147  coe1add  22199  coe1mul2lem1  22202  coe1mul2lem2  22203  coe1mul2  22204  ply1coe  22234  evls1rhmlem  22257  evl1sca  22270  evl1var  22272  pf1mpf  22288  pf1ind  22291  mat0dimscm  22405  mat0dimcrng  22406  mat0scmat  22474  mavmul0  22488  mavmul0g  22489  mvmumamul1  22490  mdet0pr  22528  mdet0f1o  22529  mdet0fv0  22530  mdetunilem9  22556  d0mat2pmat  22674  chpmat0d  22770  en1top  22920  en2top  22921  sn0topon  22934  indistopon  22937  indistps  22947  indistps2  22948  sn0cld  23026  indiscld  23027  neipeltop  23065  rest0  23105  restsn  23106  cmpfi  23344  refun0  23451  txindislem  23569  hmphindis  23733  xpstopnlem1  23745  xpstopnlem2  23747  ptcmpfi  23749  snfil  23800  fbasfip  23804  fgcl  23814  filconn  23819  fbasrn  23820  cfinfil  23829  csdfil  23830  supfil  23831  ufildr  23867  fin1aufil  23868  rnelfmlem  23888  fclsval  23944  tmdgsum  24031  tsmsfbas  24064  ust0  24156  ustn0  24157  0met  24303  xpsdsval  24318  minveclem3b  25378  tdeglem2  26016  deg1ldg  26047  deg1leb  26050  deg1val  26051  ulm0  26350  nosgnn0  27620  nodense  27654  nolt02o  27657  nogt01o  27658  nulsslt  27759  nulssgt  27760  bday1s  27793  made0  27829  precsexlem1  28148  precsexlem2  28149  uhgr0  28998  upgr0eop  29039  upgr0eopALT  29041  usgr0  29168  usgr0eop  29171  lfuhgr1v0e  29179  griedg0prc  29189  0grsubgr  29203  cplgr0  29350  0grrusgr  29505  clwwlk0on0  30019  0ewlk  30041  0wlkon  30047  0trlon  30051  0pthon  30054  0pthonv  30056  0conngr  30119  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181  wlkl0  30294  disjdifprg  32502  disjun0  32522  of0r  32602  fpwrelmapffslem  32655  f1ocnt  32725  resvsca  33294  1arithidom  33498  locfinref  33818  zarcmplem  33858  esumnul  34025  esumrnmpt2  34045  prsiga  34108  ldsysgenld  34137  ldgenpisyslem1  34140  oms0  34275  carsggect  34296  eulerpartgbij  34350  eulerpartlemmf  34353  repr0  34589  breprexp  34611  bnj941  34749  bnj97  34843  bnj149  34852  bnj150  34853  bnj944  34915  fineqvac  35074  wevgblacfn  35077  derang0  35137  indispconn  35202  goeleq12bg  35317  satf0  35340  satf0op  35345  fmla0  35350  fmla0xp  35351  fmlasuc0  35352  fmlafvel  35353  fmlasuc  35354  fmlaomn0  35358  fmla0disjsuc  35366  satfdmfmla  35368  satfv0fvfmla0  35381  sate0  35383  sate0fv0  35385  sategoelfvb  35387  ex-sategoelel  35389  prv0  35398  prv1n  35399  rdgprc  35758  dfrdg3  35760  fullfunfnv  35910  fullfunfv  35911  rank0  36134  ssoninhaus  36412  onint1  36413  bj-0nel1  36917  bj-xpnzex  36923  bj-eltag  36941  bj-0eltag  36942  bj-tagss  36944  bj-pr1val  36968  bj-snex  36999  bj-snfromadj  37008  bj-nuliota  37021  bj-nuliotaALT  37022  bj-rdg0gALT  37035  bj-rest10  37052  bj-rest10b  37053  bj-rest0  37057  rdgssun  37342  finxpreclem1  37353  finxpreclem2  37354  finxp0  37355  finxpreclem5  37359  poimirlem28  37618  heibor1lem  37779  heiborlem6  37786  reheibor  37809  n0elqs  38290  sticksstones11  42115  mzpcompact2lem  42721  wopprc  43001  pw2f1ocnv  43008  pwslnmlem0  43062  pwfi2f1o  43067  2omomeqom  43274  cantnfub  43292  cantnfresb  43295  omcl3g  43305  nadd1suc  43363  naddwordnexlem4  43372  nla0002  43395  nla0003  43396  nla0001  43397  clsk1indlem0  44012  clsk1indlem4  44015  clsk1indlem1  44016  mnupwd  44239  mnuprdlem1  44244  mnuprdlem2  44245  mnuprdlem3  44246  mnurnd  44255  permaxnul  44981  permaxinf2lem  44985  fnchoice  45001  eliuniincex  45081  limsup0  45671  0cnv  45719  liminf0  45770  0cnf  45854  dvnprodlem3  45925  qndenserrnbl  46272  prsal  46295  intsal  46307  sge00  46353  sge0sn  46356  nnfoctbdjlem  46432  isomenndlem  46507  hoiqssbl  46602  ovnsubadd2lem  46622  upwordnul  46857  iota0def  47015  aiota0def  47073  afv0fv0  47126  0nelsetpreimafv  47352  lincval0  48339  lco0  48351  linds0  48389  0aryfvalel  48562  0aryfvalelfv  48563  1aryenef  48573  2aryenef  48584  mof0  48764  dftpos5  48797  dftpos6  48798  relcic  48960  discsubclem  48978  discsubc  48979  iinfconstbas  48981  nelsubclem  48982  0funcg  48998  0func  49000  0funcALT  49001  oppfvalg  49022  oppfrcl  49024  fucofvalne  49184  0thinc  49293  setc2othin  49300  setc1ohomfval  49326  setc1ocofval  49327  isinito2lem  49331  prstcthin  49386  setc1onsubc  49427  bnd2d  49493