Theorem 0ex 5265

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

Syntax hints:  ¬ wn 3  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3450  ∅c0 4299

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-nul 4300

This theorem is referenced by:  al0ssb  5266  sseliALT  5267  csbexg  5268  unisn2  5270  class2set  5313  0elpw  5314  0nep0  5316  unidif0  5318  iin0  5320  notzfaus  5321  intv  5322  snexALT  5341  p0ex  5342  dtruALT  5346  zfpair  5379  snex  5394  opex  5427  opthwiener  5477  0sn0ep  5545  opthprc  5705  nrelv  5766  dmsnsnsn  6196  0elon  6390  nsuceq0  6420  snsn0non  6462  iotaex  6487  iotaexOLD  6494  fun0  6584  fvrn0  6891  fvssunirnOLD  6895  fprg  7130  ovima0  7571  onint0  7770  tfinds2  7843  finds  7875  finds2  7877  xpexr  7897  soex  7900  supp0  8147  fvn0elsupp  8162  fvn0elsuppb  8163  brtpos0  8215  reldmtpos  8216  tfrlem16  8364  tz7.44-1  8377  seqomlem1  8421  1n0  8455  nlim1  8456  nlim2  8457  el1o  8462  om0  8484  mapdm0  8818  fsetexb  8840  0map0sn0  8861  ixpexg  8898  0elixp  8905  en0  8992  en0ALT  8993  en0r  8994  ensn1  8995  en1  8998  2dom  9004  map1  9014  enpr2d  9023  xp1en  9031  endisj  9032  pw2eng  9052  0domg  9074  map2xp  9117  limensuci  9123  snnen2o  9191  0sdom1dom  9192  rex2dom  9200  1sdom2dom  9201  1sdomOLD  9203  unxpdom2  9208  sucxpdom  9209  isinf  9214  isinfOLD  9215  ac6sfi  9238  fodomfi  9268  fodomfiOLD  9288  0fsupp  9348  fi0  9378  oiexg  9495  brwdom  9527  brwdom2  9533  inf3lemb  9585  infeq5i  9596  dfom3  9607  cantnfvalf  9625  cantnfval2  9629  cantnfle  9631  cantnflt  9632  cantnff  9634  cantnf0  9635  cantnfp1lem1  9638  cantnfp1lem3  9640  cantnfp1  9641  cantnflem1a  9645  cantnflem1d  9648  cantnflem1  9649  cantnf  9653  cnfcomlem  9659  cnfcom  9660  cnfcom2lem  9661  cnfcom3  9664  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  dmttrcl  9681  ttrclselem2  9686  tc0  9707  r10  9728  scottex  9845  djulcl  9870  djulf1o  9872  djuss  9880  djuun  9886  1stinl  9887  2ndinl  9888  infxpenlem  9973  fseqenlem1  9984  undjudom  10128  endjudisj  10129  djuen  10130  dju1dif  10133  dju1p1e2  10134  dju0en  10136  djucomen  10138  djuassen  10139  xpdjuen  10140  mapdjuen  10141  djuxpdom  10146  djuinf  10149  infdju1  10150  djulepw  10153  pwsdompw  10163  pwdjudom  10175  ackbij1lem14  10192  ackbij2lem2  10199  ackbij2lem3  10200  cf0  10211  cfeq0  10216  cfsuc  10217  cflim2  10223  isfin5  10259  isfin4p1  10275  fin1a2lem11  10370  fin1a2lem12  10371  fin1a2lem13  10372  axcc2lem  10396  ac6num  10439  zornn0g  10465  ttukeylem3  10471  brdom3  10488  iundom2g  10500  cardeq0  10512  pwcfsdom  10543  axpowndlem3  10559  canthwe  10611  canthp1lem1  10612  pwxpndom2  10625  pwdjundom  10627  gchxpidm  10629  intwun  10695  0tsk  10715  grothomex  10789  indpi  10867  fzennn  13940  hash0  14339  hashen1  14342  hashmap  14407  hashbc  14425  hashf1  14429  hashge3el3dif  14459  ccat1st1st  14600  swrdval  14615  swrd00  14616  swrd0  14630  cshfn  14762  cshnz  14764  0csh0  14765  incexclem  15809  incexc  15810  rexpen  16203  sadcf  16430  sadc0  16431  sadcp1  16432  smupf  16455  smup0  16456  smupp1  16457  0ram  16998  ram0  17000  cshws0  17079  str0  17166  ress0  17220  0rest  17399  fnpr2ob  17528  xpsfrnel  17532  xpsle  17549  ismred2  17571  acsfn  17627  0cat  17657  ciclcl  17771  cicrcl  17772  cicer  17775  setcepi  18057  setc2obas  18063  setc2ohom  18064  cat1  18066  0pos  18289  join0  18371  meet0  18372  mgm0b  18591  gsum0  18618  sgrp0b  18662  efmnd0nmnd  18824  pwmnd  18871  mulgfval  19008  ga0  19237  psgn0fv0  19448  pmtrsn  19456  oppglsm  19579  efgi0  19657  vrgpf  19705  vrgpinv  19706  frgpuptinv  19708  frgpup2  19713  0frgp  19716  frgpnabllem1  19810  frgpnabllem2  19811  dprd0  19970  dmdprdpr  19988  dprdpr  19989  00lsp  20894  cnfldfun  21285  cnfldfunOLD  21298  frgpcyg  21490  frlmiscvec  21765  fvcoe1  22099  coe1f2  22101  coe1sfi  22105  coe1add  22157  coe1mul2lem1  22160  coe1mul2lem2  22161  coe1mul2  22162  ply1coe  22192  evls1rhmlem  22215  evl1sca  22228  evl1var  22230  pf1mpf  22246  pf1ind  22249  mat0dimscm  22363  mat0dimcrng  22364  mat0scmat  22432  mavmul0  22446  mavmul0g  22447  mvmumamul1  22448  mdet0pr  22486  mdet0f1o  22487  mdet0fv0  22488  mdetunilem9  22514  d0mat2pmat  22632  chpmat0d  22728  en1top  22878  en2top  22879  sn0topon  22892  indistopon  22895  indistps  22905  indistps2  22906  sn0cld  22984  indiscld  22985  neipeltop  23023  rest0  23063  restsn  23064  cmpfi  23302  refun0  23409  txindislem  23527  hmphindis  23691  xpstopnlem1  23703  xpstopnlem2  23705  ptcmpfi  23707  snfil  23758  fbasfip  23762  fgcl  23772  filconn  23777  fbasrn  23778  cfinfil  23787  csdfil  23788  supfil  23789  ufildr  23825  fin1aufil  23826  rnelfmlem  23846  fclsval  23902  tmdgsum  23989  tsmsfbas  24022  ust0  24114  ustn0  24115  0met  24261  xpsdsval  24276  minveclem3b  25335  tdeglem2  25973  deg1ldg  26004  deg1leb  26007  deg1val  26008  ulm0  26307  nosgnn0  27577  nodense  27611  nolt02o  27614  nogt01o  27615  nulsslt  27716  nulssgt  27717  bday1s  27750  made0  27792  precsexlem1  28116  precsexlem2  28117  uhgr0  29007  upgr0eop  29048  upgr0eopALT  29050  usgr0  29177  usgr0eop  29180  lfuhgr1v0e  29188  griedg0prc  29198  0grsubgr  29212  cplgr0  29359  0grrusgr  29514  clwwlk0on0  30028  0ewlk  30050  0wlkon  30056  0trlon  30060  0pthon  30063  0pthonv  30065  0conngr  30128  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  wlkl0  30303  disjdifprg  32511  disjun0  32531  of0r  32609  fpwrelmapffslem  32662  f1ocnt  32732  resvsca  33311  1arithidom  33515  locfinref  33838  zarcmplem  33878  esumnul  34045  esumrnmpt2  34065  prsiga  34128  ldsysgenld  34157  ldgenpisyslem1  34160  oms0  34295  carsggect  34316  eulerpartgbij  34370  eulerpartlemmf  34373  repr0  34609  breprexp  34631  bnj941  34769  bnj97  34863  bnj149  34872  bnj150  34873  bnj944  34935  fineqvac  35094  wevgblacfn  35103  derang0  35163  indispconn  35228  goeleq12bg  35343  satf0  35366  satf0op  35371  fmla0  35376  fmla0xp  35377  fmlasuc0  35378  fmlafvel  35379  fmlasuc  35380  fmlaomn0  35384  fmla0disjsuc  35392  satfdmfmla  35394  satfv0fvfmla0  35407  sate0  35409  sate0fv0  35411  sategoelfvb  35413  ex-sategoelel  35415  prv0  35424  prv1n  35425  rdgprc  35789  dfrdg3  35791  fullfunfnv  35941  fullfunfv  35942  rank0  36165  ssoninhaus  36443  onint1  36444  bj-0nel1  36948  bj-xpnzex  36954  bj-eltag  36972  bj-0eltag  36973  bj-tagss  36975  bj-pr1val  36999  bj-snex  37030  bj-snfromadj  37039  bj-nuliota  37052  bj-nuliotaALT  37053  bj-rdg0gALT  37066  bj-rest10  37083  bj-rest10b  37084  bj-rest0  37088  rdgssun  37373  finxpreclem1  37384  finxpreclem2  37385  finxp0  37386  finxpreclem5  37390  poimirlem28  37649  heibor1lem  37810  heiborlem6  37817  reheibor  37840  n0elqs  38321  sticksstones11  42151  mzpcompact2lem  42746  wopprc  43026  pw2f1ocnv  43033  pwslnmlem0  43087  pwfi2f1o  43092  2omomeqom  43299  cantnfub  43317  cantnfresb  43320  omcl3g  43330  nadd1suc  43388  naddwordnexlem4  43397  nla0002  43420  nla0003  43421  nla0001  43422  clsk1indlem0  44037  clsk1indlem4  44040  clsk1indlem1  44041  mnupwd  44263  mnuprdlem1  44268  mnuprdlem2  44269  mnuprdlem3  44270  mnurnd  44279  permaxnul  45005  permaxinf2lem  45009  nregmodelf1o  45012  nregmodellem  45013  nregmodel  45014  fnchoice  45030  eliuniincex  45110  limsup0  45699  0cnv  45747  liminf0  45798  0cnf  45882  dvnprodlem3  45953  qndenserrnbl  46300  prsal  46323  intsal  46335  sge00  46381  sge0sn  46384  nnfoctbdjlem  46460  isomenndlem  46535  hoiqssbl  46630  ovnsubadd2lem  46650  upwordnul  46885  iota0def  47043  aiota0def  47101  afv0fv0  47154  0nelsetpreimafv  47395  lincval0  48408  lco0  48420  linds0  48458  0aryfvalel  48627  0aryfvalelfv  48628  1aryenef  48638  2aryenef  48649  mof0  48830  dftpos5  48866  dftpos6  48867  relcic  49038  discsubclem  49056  discsubc  49057  iinfconstbas  49059  nelsubclem  49060  0funcg  49078  0func  49080  0funcALT  49081  oppffn  49117  oppfvalg  49119  fucofvalne  49318  0thinc  49452  setc2othin  49459  setc1ohomfval  49486  setc1ocofval  49487  isinito2lem  49491  prstcthin  49554  setc1onsubc  49595  initocmd  49662  termolmd  49663  bnd2d  49674