Theorem 0ex 5229

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 5228. (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 5228	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4278	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1855	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 232	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3450	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3431  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-nul 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-nul 4262

This theorem is referenced by:  al0ssb  5230  sseliALT  5231  csbexg  5232  unisn2  5234  class2set  5283  0elpw  5284  0nep0  5286  unidif0  5288  unidif0OLD  5289  iin0  5291  notzfaus  5292  intv  5293  snexALT  5312  p0ex  5313  dtruALT  5317  zfpair  5350  snexOLD  5371  opexOLD  5404  opthwiener  5455  0sn0ep  5522  opthprc  5682  nrelv  5743  dmsnsnsn  6171  0elon  6365  nsuceq0  6395  snsn0non  6436  iotaex  6461  fun0  6550  fvrn0  6855  fprg  7098  ovima0  7535  onint0  7734  tfinds2  7804  finds  7836  finds2  7838  xpexr  7858  soex  7861  supp0  8105  fvn0elsupp  8120  fvn0elsuppb  8121  brtpos0  8173  reldmtpos  8174  tfrlem16  8322  tz7.44-1  8335  seqomlem1  8379  1n0  8413  nlim1  8414  nlim2  8415  el1o  8420  om0  8442  mapdm0  8779  fsetexb  8801  0map0sn0  8823  ixpexg  8860  0elixp  8867  en0  8955  en0ALT  8956  en0r  8957  ensn1  8958  en1  8961  2dom  8967  map1  8977  enpr2d  8985  xp1en  8991  endisj  8992  pw2eng  9011  0domg  9032  map2xp  9075  limensuci  9081  snnen2o  9145  0sdom1dom  9146  rex2dom  9153  1sdom2dom  9154  unxpdom2  9160  sucxpdom  9161  isinf  9165  ac6sfi  9184  fodomfi  9212  fodomfiOLD  9230  0fsupp  9293  fi0  9323  oiexg  9440  brwdom  9472  brwdom2  9478  inf3lemb  9537  infeq5i  9548  dfom3  9559  cantnfvalf  9577  cantnfval2  9581  cantnfle  9583  cantnflt  9584  cantnff  9586  cantnf0  9587  cantnfp1lem1  9590  cantnfp1lem3  9592  cantnfp1  9593  cantnflem1a  9597  cantnflem1d  9600  cantnflem1  9601  cantnf  9605  cnfcomlem  9611  cnfcom  9612  cnfcom2lem  9613  cnfcom3  9616  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  dmttrcl  9633  ttrclselem2  9638  tc0  9657  r10  9683  scottex  9800  djulcl  9825  djulf1o  9827  djuss  9835  djuun  9841  1stinl  9842  2ndinl  9843  infxpenlem  9926  fseqenlem1  9937  undjudom  10081  endjudisj  10082  djuen  10083  dju1dif  10086  dju1p1e2  10087  dju0en  10089  djucomen  10091  djuassen  10092  xpdjuen  10093  mapdjuen  10094  djuxpdom  10099  djuinf  10102  infdju1  10103  djulepw  10106  pwsdompw  10116  pwdjudom  10128  ackbij1lem14  10145  ackbij2lem2  10152  ackbij2lem3  10153  cf0  10164  cfeq0  10169  cfsuc  10170  cflim2  10176  isfin5  10212  isfin4p1  10228  fin1a2lem11  10323  fin1a2lem12  10324  fin1a2lem13  10325  axcc2lem  10349  ac6num  10392  zornn0g  10418  ttukeylem3  10424  brdom3  10441  iundom2g  10453  cardeq0  10465  pwcfsdom  10497  axpowndlem3  10513  canthwe  10565  canthp1lem1  10566  pwxpndom2  10579  pwdjundom  10581  gchxpidm  10583  intwun  10649  0tsk  10669  grothomex  10743  indpi  10821  fzennn  13921  hash0  14320  hashen1  14323  hashmap  14388  hashbc  14406  hashf1  14410  hashge3el3dif  14440  ccat1st1st  14582  swrdval  14597  swrd00  14598  swrd0  14612  cshfn  14743  cshnz  14745  0csh0  14746  incexclem  15792  incexc  15793  rexpen  16186  sadcf  16413  sadc0  16414  sadcp1  16415  smupf  16438  smup0  16439  smupp1  16440  0ram  16982  ram0  16984  cshws0  17063  str0  17150  ress0  17204  0rest  17383  fnpr2ob  17513  xpsfrnel  17517  xpsle  17534  ismred2  17556  acsfn  17616  0cat  17646  ciclcl  17760  cicrcl  17761  cicer  17764  setcepi  18046  setc2obas  18052  setc2ohom  18053  cat1  18055  0pos  18278  join0  18360  meet0  18361  mgm0b  18616  gsum0  18643  sgrp0b  18687  efmnd0nmnd  18849  pwmnd  18899  mulgfval  19036  ga0  19264  psgn0fv0  19477  pmtrsn  19485  oppglsm  19608  efgi0  19686  vrgpf  19734  vrgpinv  19735  frgpuptinv  19737  frgpup2  19742  0frgp  19745  frgpnabllem1  19839  frgpnabllem2  19840  dprd0  19999  dmdprdpr  20017  dprdpr  20018  00lsp  20971  cnfldfun  21361  frgpcyg  21548  frlmiscvec  21824  fvcoe1  22192  coe1f2  22194  coe1sfi  22198  coe1add  22250  coe1mul2lem1  22253  coe1mul2lem2  22254  coe1mul2  22255  ply1coe  22284  evls1rhmlem  22307  evl1sca  22320  evl1var  22322  pf1mpf  22338  pf1ind  22341  mat0dimscm  22452  mat0dimcrng  22453  mat0scmat  22521  mavmul0  22535  mavmul0g  22536  mvmumamul1  22537  mdet0pr  22575  mdet0f1o  22576  mdet0fv0  22577  mdetunilem9  22603  d0mat2pmat  22721  chpmat0d  22817  en1top  22967  en2top  22968  sn0topon  22981  indistopon  22984  indistps  22994  indistps2  22995  sn0cld  23073  indiscld  23074  neipeltop  23112  rest0  23152  restsn  23153  cmpfi  23391  refun0  23498  txindislem  23616  hmphindis  23780  xpstopnlem1  23792  xpstopnlem2  23794  ptcmpfi  23796  snfil  23847  fbasfip  23851  fgcl  23861  filconn  23866  fbasrn  23867  cfinfil  23876  csdfil  23877  supfil  23878  ufildr  23914  fin1aufil  23915  rnelfmlem  23935  fclsval  23991  tmdgsum  24078  tsmsfbas  24111  ust0  24203  ustn0  24204  0met  24349  xpsdsval  24364  minveclem3b  25413  tdeglem2  26044  deg1ldg  26075  deg1leb  26078  deg1val  26079  ulm0  26374  nosgnn0  27640  nodense  27674  nolt02o  27677  nogt01o  27678  nulslts  27785  nulsgts  27786  bday1  27824  made0  27873  precsexlem1  28217  precsexlem2  28218  uhgr0  29160  upgr0eop  29201  upgr0eopALT  29203  usgr0  29330  usgr0eop  29333  lfuhgr1v0e  29341  griedg0prc  29351  0grsubgr  29365  cplgr0  29512  0grrusgr  29666  clwwlk0on0  30180  0ewlk  30202  0wlkon  30208  0trlon  30212  0pthon  30215  0pthonv  30217  0conngr  30280  konigsberglem1  30340  konigsberglem2  30341  konigsberglem3  30342  wlkl0  30455  disjdifprg  32664  disjun0  32684  of0r  32771  fpwrelmapffslem  32824  f1ocnt  32892  resvsca  33415  1arithidom  33620  0mplrim  33698  selvply1rhmlema  33702  selvply1rhmlemb  33703  selvply1rhmlem1  33704  selvply1rhm0  33710  mplidomlem  33711  vieta  33764  locfinref  34025  zarcmplem  34065  esumnul  34232  esumrnmpt2  34252  prsiga  34315  ldsysgenld  34344  ldgenpisyslem1  34347  oms0  34481  carsggect  34502  eulerpartgbij  34556  eulerpartlemmf  34559  repr0  34795  breprexp  34817  bnj941  34955  bnj97  35048  bnj149  35057  bnj150  35058  bnj944  35120  fineqvac  35297  fineqvnttrclse  35305  wevgblacfn  35337  derang0  35397  indispconn  35462  goeleq12bg  35577  satf0  35600  satf0op  35605  fmla0  35610  fmla0xp  35611  fmlasuc0  35612  fmlafvel  35613  fmlasuc  35614  fmlaomn0  35618  fmla0disjsuc  35626  satfdmfmla  35628  satfv0fvfmla0  35641  sate0  35643  sate0fv0  35645  sategoelfvb  35647  ex-sategoelel  35649  prv0  35658  prv1n  35659  rdgprc  36020  dfrdg3  36022  fullfunfnv  36174  fullfunfv  36175  rank0  36398  ssoninhaus  36676  onint1  36677  mh-infprim2bi  36775  bj-0nel1  37306  bj-xpnzex  37312  bj-eltag  37330  bj-0eltag  37331  bj-tagss  37333  bj-pr1val  37357  bj-snex  37388  bj-snfromadj  37397  bj-nuliota  37410  bj-nuliotaALT  37411  bj-rdg0gALT  37424  bj-rest10  37446  bj-rest10b  37447  bj-rest0  37451  rdgssun  37740  finxpreclem1  37751  finxpreclem2  37752  finxp0  37753  finxpreclem5  37757  poimirlem28  38015  heibor1lem  38176  heiborlem6  38183  reheibor  38206  n0elqs  38699  sticksstones11  42641  mzpcompact2lem  43200  wopprc  43475  pw2f1ocnv  43482  pwslnmlem0  43536  pwfi2f1o  43541  2omomeqom  43748  cantnfub  43766  cantnfresb  43769  omcl3g  43779  nadd1suc  43837  naddwordnexlem4  43846  nla0002  43868  nla0003  43869  nla0001  43870  clsk1indlem0  44485  clsk1indlem4  44488  clsk1indlem1  44489  mnupwd  44711  mnuprdlem1  44716  mnuprdlem2  44717  mnuprdlem3  44718  mnurnd  44727  permaxnul  45452  permaxinf2lem  45456  nregmodelf1o  45459  nregmodellem  45460  nregmodel  45461  fnchoice  45477  eliuniincex  45556  limsup0  46137  0cnv  46185  liminf0  46236  0cnf  46320  dvnprodlem3  46391  qndenserrnbl  46738  prsal  46761  intsal  46773  sge00  46819  sge0sn  46822  nnfoctbdjlem  46898  isomenndlem  46973  hoiqssbl  47068  ovnsubadd2lem  47088  iota0def  47501  aiota0def  47559  afv0fv0  47612  0nelsetpreimafv  47865  lincval0  48906  lco0  48918  linds0  48956  0aryfvalel  49125  0aryfvalelfv  49126  1aryenef  49136  2aryenef  49147  mof0  49328  dftpos5  49364  dftpos6  49365  relcic  49535  discsubclem  49553  discsubc  49554  iinfconstbas  49556  nelsubclem  49557  0funcg  49575  0func  49577  0funcALT  49578  oppffn  49614  oppfvalg  49616  fucofvalne  49815  0thinc  49949  setc2othin  49956  setc1ohomfval  49983  setc1ocofval  49984  isinito2lem  49988  prstcthin  50051  setc1onsubc  50092  initocmd  50159  termolmd  50160  bnd2d  50171