Theorem 0ex 5271

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

Syntax hints:  ¬ wn 3  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-nul 4288

This theorem is referenced by:  al0ssb  5272  sseliALT  5273  csbexg  5274  unisn2  5276  class2set  5327  0elpw  5328  0nep0  5330  unidif0  5332  unidif0OLD  5333  iin0  5335  notsep  5336  intv  5337  snexALT  5356  p0ex  5357  dtruALT  5361  zfpair  5394  snexOLD  5415  opexOLD  5448  opthwiener  5499  0sn0ep  5567  opthprc  5727  nrelv  5788  nrelvOLD  5789  dmsnsnsn  6223  0elon  6418  nsuceq0  6448  snsn0non  6489  iotaex  6514  fun0  6603  fvrn0  6911  fprg  7154  ovima0  7591  onint0  7791  tfinds2  7861  finds  7894  finds2  7896  xpexr  7916  soex  7919  supp0  8162  fvn0elsupp  8177  fvn0elsuppb  8178  brtpos0  8230  reldmtpos  8231  tfrlem16  8381  tz7.44-1  8394  seqomlem1  8438  1n0OLD  8474  nlim1  8475  nlim2  8476  el1o  8481  om0  8503  mapdm0  8840  fsetexb  8862  0map0sn0  8884  ixpexg  8921  0elixp  8928  en0  9016  en0ALT  9017  en0r  9018  ensn1  9019  en1  9022  2dom  9028  map1  9038  enpr2d  9046  xp1en  9052  endisj  9053  pw2eng  9072  0domg  9093  map2xp  9136  limensuci  9142  snnen2o  9206  0sdom1dom  9207  rex2dom  9214  1sdom2dom  9215  unxpdom2  9221  sucxpdom  9222  isinf  9226  ac6sfi  9245  fodomfi  9273  0fsupp  9351  fi0  9381  oiexg  9498  brwdom  9530  brwdom2  9536  inf3lemb  9595  infeq5i  9606  dfom3  9617  cantnfvalf  9635  cantnfval2  9639  cantnfle  9641  cantnflt  9642  cantnff  9644  cantnf0  9645  cantnfp1lem1  9648  cantnfp1lem3  9650  cantnfp1  9651  cantnflem1a  9655  cantnflem1d  9658  cantnflem1  9659  cantnf  9663  cnfcomlem  9669  cnfcom  9670  cnfcom2lem  9671  cnfcom3  9674  ssttrcl  9685  ttrcltr  9686  ttrclss  9690  dmttrcl  9691  ttrclselem2  9696  tc0  9715  r10  9741  scottex  9860  djulcl  9897  djulf1o  9899  djuss  9907  djuun  9913  1stinl  9914  2ndinl  9915  infxpenlem  9998  fseqenlem1  10009  undjudom  10152  endjudisj  10153  djuen  10154  dju1dif  10157  dju1p1e2  10158  dju0en  10160  djucomen  10162  djuassen  10163  xpdjuen  10164  mapdjuen  10165  djuxpdom  10170  djuinf  10173  infdju1  10174  djulepw  10177  pwsdompw  10187  pwdjudom  10199  ackbij1lem14  10216  ackbij2lem2  10223  ackbij2lem3  10224  cf0  10235  cfeq0  10241  cfsuc  10242  cflim2  10248  isfin5  10284  isfin4p1  10300  fin1a2lem11  10395  fin1a2lem12  10396  fin1a2lem13  10397  axcc2lem  10421  ac6num  10464  zornn0g  10490  ttukeylem3  10496  brdom3  10513  iundom2g  10525  cardeq0  10537  pwcfsdom  10569  axpowndlem3  10585  canthwe  10637  canthp1lem1  10638  pwxpndom2  10651  pwdjundom  10653  gchxpidm  10655  intwun  10721  0tsk  10741  grothomex  10815  indpi  10893  fzennn  14006  hash0  14405  hashen1  14408  hashmap  14474  hashbc  14492  hashf1  14496  hashge3el3dif  14526  ccat1st1st  14668  swrdval  14683  swrd00  14684  swrd0  14698  cshfn  14829  cshnz  14831  0csh0  14832  incexclem  15892  incexc  15893  rexpen  16285  sadcf  16512  sadc0  16513  sadcp1  16514  smupf  16537  smup0  16538  smupp1  16539  0ram  17081  ram0  17083  cshws0  17162  str0  17250  ress0  17304  0rest  17483  fnpr2ob  17613  xpsfrnel  17617  xpsle  17634  ismred2  17656  acsfn  17716  0cat  17746  ciclcl  17860  cicrcl  17861  cicer  17864  setcepi  18146  setc2obas  18152  setc2ohom  18153  cat1  18155  0pos  18378  join0  18460  meet0  18461  mgm0b  18716  gsum0  18743  sgrp0b  18787  efmnd0nmnd  18950  pwmnd  19000  mulgfval  19136  ga0  19369  psgn0fv0  19582  pmtrsn  19590  oppglsm  19713  efgi0  19791  vrgpf  19839  vrgpinv  19840  frgpuptinv  19842  frgpup2  19847  0frgp  19850  frgpnabllem1  19944  frgpnabllem2  19945  dprd0  20104  dmdprdpr  20122  dprdpr  20123  00lsp  21083  cnfldfun  21517  frgpcyg  21704  frlmiscvec  21980  fvcoe1  22348  coe1f2  22350  coe1sfi  22354  coe1add  22406  coe1mul2lem1  22409  coe1mul2lem2  22410  coe1mul2  22411  ply1coe  22439  evls1rhmlem  22462  evl1sca  22475  evl1var  22477  pf1mpf  22493  pf1ind  22496  mat0dimscm  22607  mat0dimcrng  22608  mat0scmat  22676  mavmul0  22690  mavmul0g  22691  mvmumamul1  22692  mdet0pr  22730  mdet0f1o  22731  mdet0fv0  22732  mdetunilem9  22758  d0mat2pmat  22876  chpmat0d  22972  en1top  23122  en2top  23123  sn0topon  23136  indistopon  23139  indistps  23149  indistps2  23150  sn0cld  23228  indiscld  23229  neipeltop  23267  rest0  23307  restsn  23308  cmpfi  23546  refun0  23653  txindislem  23771  hmphindis  23935  xpstopnlem1  23947  xpstopnlem2  23949  ptcmpfi  23951  snfil  24002  fbasfip  24006  fgcl  24016  filconn  24021  fbasrn  24022  cfinfil  24031  csdfil  24032  supfil  24033  ufildr  24069  fin1aufil  24070  rnelfmlem  24090  fclsval  24146  tmdgsum  24233  tsmsfbas  24266  ust0  24358  ustn0  24359  0met  24504  xpsdsval  24519  minveclem3b  25568  tdeglem2  26199  deg1ldg  26230  deg1leb  26233  deg1val  26234  ulm0  26535  nosgnn0  27803  nodense  27837  nolt02o  27840  nogt01o  27841  nulslts  27949  nulsgts  27950  bday1  27988  made0  28037  precsexlem1  28381  precsexlem2  28382  uhgr0  29404  upgr0eop  29445  upgr0eopALT  29447  usgr0  29574  usgr0eop  29577  lfuhgr1v0e  29585  griedg0prc  29595  0grsubgr  29609  cplgr0  29756  0grrusgr  29910  clwwlk0on0  30424  0ewlk  30446  0wlkon  30452  0trlon  30456  0pthon  30459  0pthonv  30461  0conngr  30524  konigsberglem1  30584  konigsberglem2  30585  konigsberglem3  30586  wlkl0  30699  disjdifprg  32901  disjun0  32921  of0r  33005  fpwrelmapffslem  33058  f1ocnt  33126  resvsca  33633  1arithidom  33808  0mplrim  33885  selvply1rhmlema  33889  selvply1rhmlemb  33890  selvply1rhmlem1  33891  selvply1rhm0  33897  mplidomlem  33898  vieta  33951  locfinref  34212  zarcmplem  34252  esumnul  34419  esumrnmpt2  34439  prsiga  34502  ldsysgenld  34531  ldgenpisyslem1  34534  oms0  34668  carsggect  34689  eulerpartgbij  34743  eulerpartlemmf  34746  repr0  34979  breprexp  35001  bnj941  35142  bnj97  35235  bnj149  35244  bnj150  35245  bnj944  35307  fineqvac  35510  fineqvnttrclse  35518  kard0  35548  kard0b  35553  wevgblacfn  35576  derang0  35642  indispconn  35707  goeleq12bg  35822  satf0  35845  satf0op  35850  fmla0  35855  fmla0xp  35856  fmlasuc0  35857  fmlafvel  35858  fmlasuc  35859  fmlaomn0  35863  fmla0disjsuc  35871  satfdmfmla  35873  satfv0fvfmla0  35886  sate0  35888  sate0fv0  35890  sategoelfvb  35892  ex-sategoelel  35894  prv0  35903  prv1n  35904  rdgprc  36265  dfrdg3  36267  fullfunfnv  36419  fullfunfv  36420  rank0  36643  nmulrid  36678  ssoninhaus  36940  onint1  36941  mh-infprim2bi  37039  bj-0nel1  37570  bj-xpnzex  37576  bj-eltag  37594  bj-0eltag  37595  bj-tagss  37597  bj-pr1val  37621  bj-snex  37652  bj-snfromadj  37661  bj-nuliota  37674  bj-nuliotaALT  37675  bj-rdg0gALT  37688  bj-rest10  37711  bj-rest10b  37712  bj-rest0  37716  rdgssun  38005  finxpreclem1  38016  finxpreclem2  38017  finxp0  38018  finxpreclem5  38022  poimirlem28  38280  heibor1lem  38441  heiborlem6  38448  reheibor  38471  n0elqs  38962  sticksstones11  42904  mzpcompact2lem  43465  wopprc  43740  pw2f1ocnv  43747  pwslnmlem0  43801  pwfi2f1o  43806  2omomeqom  44013  cantnfub  44031  cantnfresb  44034  omcl3g  44044  nadd1suc  44102  naddwordnexlem4  44111  nla0002  44133  nla0003  44134  nla0001  44135  clsk1indlem0  44750  clsk1indlem4  44753  clsk1indlem1  44754  mnupwd  44960  mnuprdlem1  44965  mnuprdlem2  44966  mnuprdlem3  44967  mnurnd  44976  permaxnul  45700  permaxinf2lem  45704  nregmodelf1o  45707  nregmodellem  45708  nregmodel  45709  fnchoice  45732  eliuniincex  45810  limsup0  46391  0cnv  46439  liminf0  46490  0cnf  46574  dvnprodlem3  46645  qndenserrnbl  46992  prsal  47015  intsal  47027  sge00  47073  sge0sn  47076  nnfoctbdjlem  47152  isomenndlem  47227  hoiqssbl  47322  ovnsubadd2lem  47342  iota0def  47758  aiota0def  47816  afv0fv0  47869  0nelsetpreimafv  48122  lincval0  49178  lco0  49190  linds0  49228  0aryfvalel  49397  0aryfvalelfv  49398  1aryenef  49408  2aryenef  49419  mof0  49599  dftpos5  49635  dftpos6  49636  relcic  49806  discsubclem  49824  discsubc  49825  iinfconstbas  49827  nelsubclem  49828  0funcg  49846  0func  49848  0funcALT  49849  oppffn  49885  oppfvalg  49887  fucofvalne  50086  0thinc  50220  setc2othin  50227  setc1ohomfval  50254  setc1ocofval  50255  isinito2lem  50259  prstcthin  50322  setc1onsubc  50363  initocmd  50430  termolmd  50431  bnd2d  50442