Theorem 0ex 5262

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

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

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 2701  ax-nul 5261

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-nul 4297

This theorem is referenced by:  al0ssb  5263  sseliALT  5264  csbexg  5265  unisn2  5267  class2set  5310  0elpw  5311  0nep0  5313  unidif0  5315  iin0  5317  notzfaus  5318  intv  5319  snexALT  5338  p0ex  5339  dtruALT  5343  zfpair  5376  snex  5391  opex  5424  opthwiener  5474  0sn0ep  5542  opthprc  5702  nrelv  5763  dmsnsnsn  6193  0elon  6387  nsuceq0  6417  snsn0non  6459  iotaex  6484  iotaexOLD  6491  fun0  6581  fvrn0  6888  fvssunirnOLD  6892  fprg  7127  ovima0  7568  onint0  7767  tfinds2  7840  finds  7872  finds2  7874  xpexr  7894  soex  7897  supp0  8144  fvn0elsupp  8159  fvn0elsuppb  8160  brtpos0  8212  reldmtpos  8213  tfrlem16  8361  tz7.44-1  8374  seqomlem1  8418  1n0  8452  nlim1  8453  nlim2  8454  el1o  8459  om0  8481  mapdm0  8815  fsetexb  8837  0map0sn0  8858  ixpexg  8895  0elixp  8902  en0  8989  en0ALT  8990  en0r  8991  ensn1  8992  en1  8995  2dom  9001  map1  9011  enpr2d  9020  xp1en  9027  endisj  9028  pw2eng  9047  0domg  9068  map2xp  9111  limensuci  9117  snnen2o  9184  0sdom1dom  9185  rex2dom  9193  1sdom2dom  9194  1sdomOLD  9196  unxpdom2  9201  sucxpdom  9202  isinf  9207  isinfOLD  9208  ac6sfi  9231  fodomfi  9261  fodomfiOLD  9281  0fsupp  9341  fi0  9371  oiexg  9488  brwdom  9520  brwdom2  9526  inf3lemb  9578  infeq5i  9589  dfom3  9600  cantnfvalf  9618  cantnfval2  9622  cantnfle  9624  cantnflt  9625  cantnff  9627  cantnf0  9628  cantnfp1lem1  9631  cantnfp1lem3  9633  cantnfp1  9634  cantnflem1a  9638  cantnflem1d  9641  cantnflem1  9642  cantnf  9646  cnfcomlem  9652  cnfcom  9653  cnfcom2lem  9654  cnfcom3  9657  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  dmttrcl  9674  ttrclselem2  9679  tc0  9700  r10  9721  scottex  9838  djulcl  9863  djulf1o  9865  djuss  9873  djuun  9879  1stinl  9880  2ndinl  9881  infxpenlem  9966  fseqenlem1  9977  undjudom  10121  endjudisj  10122  djuen  10123  dju1dif  10126  dju1p1e2  10127  dju0en  10129  djucomen  10131  djuassen  10132  xpdjuen  10133  mapdjuen  10134  djuxpdom  10139  djuinf  10142  infdju1  10143  djulepw  10146  pwsdompw  10156  pwdjudom  10168  ackbij1lem14  10185  ackbij2lem2  10192  ackbij2lem3  10193  cf0  10204  cfeq0  10209  cfsuc  10210  cflim2  10216  isfin5  10252  isfin4p1  10268  fin1a2lem11  10363  fin1a2lem12  10364  fin1a2lem13  10365  axcc2lem  10389  ac6num  10432  zornn0g  10458  ttukeylem3  10464  brdom3  10481  iundom2g  10493  cardeq0  10505  pwcfsdom  10536  axpowndlem3  10552  canthwe  10604  canthp1lem1  10605  pwxpndom2  10618  pwdjundom  10620  gchxpidm  10622  intwun  10688  0tsk  10708  grothomex  10782  indpi  10860  fzennn  13933  hash0  14332  hashen1  14335  hashmap  14400  hashbc  14418  hashf1  14422  hashge3el3dif  14452  ccat1st1st  14593  swrdval  14608  swrd00  14609  swrd0  14623  cshfn  14755  cshnz  14757  0csh0  14758  incexclem  15802  incexc  15803  rexpen  16196  sadcf  16423  sadc0  16424  sadcp1  16425  smupf  16448  smup0  16449  smupp1  16450  0ram  16991  ram0  16993  cshws0  17072  str0  17159  ress0  17213  0rest  17392  fnpr2ob  17521  xpsfrnel  17525  xpsle  17542  ismred2  17564  acsfn  17620  0cat  17650  ciclcl  17764  cicrcl  17765  cicer  17768  setcepi  18050  setc2obas  18056  setc2ohom  18057  cat1  18059  0pos  18282  join0  18364  meet0  18365  mgm0b  18584  gsum0  18611  sgrp0b  18655  efmnd0nmnd  18817  pwmnd  18864  mulgfval  19001  ga0  19230  psgn0fv0  19441  pmtrsn  19449  oppglsm  19572  efgi0  19650  vrgpf  19698  vrgpinv  19699  frgpuptinv  19701  frgpup2  19706  0frgp  19709  frgpnabllem1  19803  frgpnabllem2  19804  dprd0  19963  dmdprdpr  19981  dprdpr  19982  00lsp  20887  cnfldfun  21278  cnfldfunOLD  21291  frgpcyg  21483  frlmiscvec  21758  fvcoe1  22092  coe1f2  22094  coe1sfi  22098  coe1add  22150  coe1mul2lem1  22153  coe1mul2lem2  22154  coe1mul2  22155  ply1coe  22185  evls1rhmlem  22208  evl1sca  22221  evl1var  22223  pf1mpf  22239  pf1ind  22242  mat0dimscm  22356  mat0dimcrng  22357  mat0scmat  22425  mavmul0  22439  mavmul0g  22440  mvmumamul1  22441  mdet0pr  22479  mdet0f1o  22480  mdet0fv0  22481  mdetunilem9  22507  d0mat2pmat  22625  chpmat0d  22721  en1top  22871  en2top  22872  sn0topon  22885  indistopon  22888  indistps  22898  indistps2  22899  sn0cld  22977  indiscld  22978  neipeltop  23016  rest0  23056  restsn  23057  cmpfi  23295  refun0  23402  txindislem  23520  hmphindis  23684  xpstopnlem1  23696  xpstopnlem2  23698  ptcmpfi  23700  snfil  23751  fbasfip  23755  fgcl  23765  filconn  23770  fbasrn  23771  cfinfil  23780  csdfil  23781  supfil  23782  ufildr  23818  fin1aufil  23819  rnelfmlem  23839  fclsval  23895  tmdgsum  23982  tsmsfbas  24015  ust0  24107  ustn0  24108  0met  24254  xpsdsval  24269  minveclem3b  25328  tdeglem2  25966  deg1ldg  25997  deg1leb  26000  deg1val  26001  ulm0  26300  nosgnn0  27570  nodense  27604  nolt02o  27607  nogt01o  27608  nulsslt  27709  nulssgt  27710  bday1s  27743  made0  27785  precsexlem1  28109  precsexlem2  28110  uhgr0  29000  upgr0eop  29041  upgr0eopALT  29043  usgr0  29170  usgr0eop  29173  lfuhgr1v0e  29181  griedg0prc  29191  0grsubgr  29205  cplgr0  29352  0grrusgr  29507  clwwlk0on0  30021  0ewlk  30043  0wlkon  30049  0trlon  30053  0pthon  30056  0pthonv  30058  0conngr  30121  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  wlkl0  30296  disjdifprg  32504  disjun0  32524  of0r  32602  fpwrelmapffslem  32655  f1ocnt  32725  resvsca  33304  1arithidom  33508  locfinref  33831  zarcmplem  33871  esumnul  34038  esumrnmpt2  34058  prsiga  34121  ldsysgenld  34150  ldgenpisyslem1  34153  oms0  34288  carsggect  34309  eulerpartgbij  34363  eulerpartlemmf  34366  repr0  34602  breprexp  34624  bnj941  34762  bnj97  34856  bnj149  34865  bnj150  34866  bnj944  34928  fineqvac  35087  wevgblacfn  35096  derang0  35156  indispconn  35221  goeleq12bg  35336  satf0  35359  satf0op  35364  fmla0  35369  fmla0xp  35370  fmlasuc0  35371  fmlafvel  35372  fmlasuc  35373  fmlaomn0  35377  fmla0disjsuc  35385  satfdmfmla  35387  satfv0fvfmla0  35400  sate0  35402  sate0fv0  35404  sategoelfvb  35406  ex-sategoelel  35408  prv0  35417  prv1n  35418  rdgprc  35782  dfrdg3  35784  fullfunfnv  35934  fullfunfv  35935  rank0  36158  ssoninhaus  36436  onint1  36437  bj-0nel1  36941  bj-xpnzex  36947  bj-eltag  36965  bj-0eltag  36966  bj-tagss  36968  bj-pr1val  36992  bj-snex  37023  bj-snfromadj  37032  bj-nuliota  37045  bj-nuliotaALT  37046  bj-rdg0gALT  37059  bj-rest10  37076  bj-rest10b  37077  bj-rest0  37081  rdgssun  37366  finxpreclem1  37377  finxpreclem2  37378  finxp0  37379  finxpreclem5  37383  poimirlem28  37642  heibor1lem  37803  heiborlem6  37810  reheibor  37833  n0elqs  38314  sticksstones11  42144  mzpcompact2lem  42739  wopprc  43019  pw2f1ocnv  43026  pwslnmlem0  43080  pwfi2f1o  43085  2omomeqom  43292  cantnfub  43310  cantnfresb  43313  omcl3g  43323  nadd1suc  43381  naddwordnexlem4  43390  nla0002  43413  nla0003  43414  nla0001  43415  clsk1indlem0  44030  clsk1indlem4  44033  clsk1indlem1  44034  mnupwd  44256  mnuprdlem1  44261  mnuprdlem2  44262  mnuprdlem3  44263  mnurnd  44272  permaxnul  44998  permaxinf2lem  45002  nregmodelf1o  45005  nregmodellem  45006  nregmodel  45007  fnchoice  45023  eliuniincex  45103  limsup0  45692  0cnv  45740  liminf0  45791  0cnf  45875  dvnprodlem3  45946  qndenserrnbl  46293  prsal  46316  intsal  46328  sge00  46374  sge0sn  46377  nnfoctbdjlem  46453  isomenndlem  46528  hoiqssbl  46623  ovnsubadd2lem  46643  upwordnul  46878  iota0def  47039  aiota0def  47097  afv0fv0  47150  0nelsetpreimafv  47391  lincval0  48404  lco0  48416  linds0  48454  0aryfvalel  48623  0aryfvalelfv  48624  1aryenef  48634  2aryenef  48645  mof0  48826  dftpos5  48862  dftpos6  48863  relcic  49034  discsubclem  49052  discsubc  49053  iinfconstbas  49055  nelsubclem  49056  0funcg  49074  0func  49076  0funcALT  49077  oppffn  49113  oppfvalg  49115  fucofvalne  49314  0thinc  49448  setc2othin  49455  setc1ohomfval  49482  setc1ocofval  49483  isinito2lem  49487  prstcthin  49550  setc1onsubc  49591  initocmd  49658  termolmd  49659  bnd2d  49670