Theorem 0ex 5308

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 5307. (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 5307	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4344	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1851	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3491	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1540   = wceq 1542  ∃wex 1782   ∈ wcel 2107  Vcvv 3475  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-nul 4324

This theorem is referenced by:  al0ssb  5309  sseliALT  5310  csbexg  5311  unisn2  5313  class2set  5354  0elpw  5355  0nep0  5357  unidif0  5359  iin0  5361  notzfaus  5362  intv  5363  snexALT  5382  p0ex  5383  dtruALT  5387  zfpair  5420  snex  5432  opex  5465  opthwiener  5515  0sn0ep  5585  opthprc  5741  nrelv  5801  dmsnsnsn  6220  0elon  6419  nsuceq0  6448  snsn0non  6490  iotaex  6517  iotaexOLD  6524  fun0  6614  fvrn0  6922  fvssunirnOLD  6926  fprg  7153  ovima0  7586  onint0  7779  tfinds2  7853  finds  7889  finds2  7891  xpexr  7909  soex  7912  supp0  8151  fvn0elsupp  8165  fvn0elsuppb  8166  brtpos0  8218  reldmtpos  8219  tfrlem16  8393  tz7.44-1  8406  seqomlem1  8450  1n0  8488  nlim1  8489  nlim2  8490  el1o  8495  om0  8517  mapdm0  8836  fsetexb  8858  0map0sn0  8879  ixpexg  8916  0elixp  8923  en0  9013  en0OLD  9014  en0ALT  9015  en0r  9016  ensn1  9017  ensn1OLD  9018  en1  9021  en1OLD  9022  2dom  9030  map1  9040  enpr2d  9049  xp1en  9057  endisj  9058  pw2eng  9078  0domg  9100  map2xp  9147  limensuci  9153  snnen2o  9237  0sdom1dom  9238  rex2dom  9246  1sdom2dom  9247  1sdomOLD  9249  unxpdom2  9254  sucxpdom  9255  isinf  9260  isinfOLD  9261  ac6sfi  9287  fodomfi  9325  0fsupp  9385  fi0  9415  oiexg  9530  brwdom  9562  brwdom2  9568  inf3lemb  9620  infeq5i  9631  dfom3  9642  cantnfvalf  9660  cantnfval2  9664  cantnfle  9666  cantnflt  9667  cantnff  9669  cantnf0  9670  cantnfp1lem1  9673  cantnfp1lem3  9675  cantnfp1  9676  cantnflem1a  9680  cantnflem1d  9683  cantnflem1  9684  cantnf  9688  cnfcomlem  9694  cnfcom  9695  cnfcom2lem  9696  cnfcom3  9699  ssttrcl  9710  ttrcltr  9711  ttrclss  9715  dmttrcl  9716  ttrclselem2  9721  tc0  9742  r10  9763  scottex  9880  djulcl  9905  djulf1o  9907  djuss  9915  djuun  9921  1stinl  9922  2ndinl  9923  infxpenlem  10008  fseqenlem1  10019  undjudom  10162  endjudisj  10163  djuen  10164  dju1dif  10167  dju1p1e2  10168  dju0en  10170  djucomen  10172  djuassen  10173  xpdjuen  10174  mapdjuen  10175  djuxpdom  10180  djuinf  10183  infdju1  10184  djulepw  10187  pwsdompw  10199  pwdjudom  10211  ackbij1lem14  10228  ackbij2lem2  10235  ackbij2lem3  10236  cf0  10246  cfeq0  10251  cfsuc  10252  cflim2  10258  isfin5  10294  isfin4p1  10310  fin1a2lem11  10405  fin1a2lem12  10406  fin1a2lem13  10407  axcc2lem  10431  ac6num  10474  zornn0g  10500  ttukeylem3  10506  brdom3  10523  iundom2g  10535  cardeq0  10547  pwcfsdom  10578  axpowndlem3  10594  canthwe  10646  canthp1lem1  10647  pwxpndom2  10660  pwdjundom  10662  gchxpidm  10664  intwun  10730  0tsk  10750  grothomex  10824  indpi  10902  fzennn  13933  hash0  14327  hashen1  14330  hashmap  14395  hashbc  14412  hashf1  14418  hashge3el3dif  14447  ccat1st1st  14578  swrdval  14593  swrd00  14594  swrd0  14608  cshfn  14740  cshnz  14742  0csh0  14743  incexclem  15782  incexc  15783  rexpen  16171  sadcf  16394  sadc0  16395  sadcp1  16396  smupf  16419  smup0  16420  smupp1  16421  0ram  16953  ram0  16955  cshws0  17035  str0  17122  ressbasOLD  17180  ress0  17188  0rest  17375  fnpr2ob  17504  xpsfrnel  17508  xpsle  17525  ismred2  17547  acsfn  17603  0cat  17633  ciclcl  17749  cicrcl  17750  cicer  17753  setcepi  18038  setc2obas  18044  setc2ohom  18045  cat1  18047  0pos  18274  0posOLD  18275  join0  18358  meet0  18359  mgm0b  18576  gsum0  18603  sgrp0b  18619  efmnd0nmnd  18771  pwmnd  18818  mulgfval  18952  ga0  19162  psgn0fv0  19379  pmtrsn  19387  oppglsm  19510  efgi0  19588  vrgpf  19636  vrgpinv  19637  frgpuptinv  19639  frgpup2  19644  0frgp  19647  frgpnabllem1  19741  frgpnabllem2  19742  dprd0  19901  dmdprdpr  19919  dprdpr  19920  00lsp  20592  cnfldfun  20956  frgpcyg  21129  frlmiscvec  21404  fvcoe1  21731  coe1f2  21733  coe1sfi  21737  coe1add  21786  coe1mul2lem1  21789  coe1mul2lem2  21790  coe1mul2  21791  ply1coe  21820  evls1rhmlem  21840  evl1sca  21853  evl1var  21855  pf1mpf  21871  pf1ind  21874  mat0dimscm  21971  mat0dimcrng  21972  mat0scmat  22040  mavmul0  22054  mavmul0g  22055  mvmumamul1  22056  mdet0pr  22094  mdet0f1o  22095  mdet0fv0  22096  mdetunilem9  22122  d0mat2pmat  22240  chpmat0d  22336  en1top  22487  en2top  22488  sn0topon  22501  indistopon  22504  indistps  22514  indistps2  22515  sn0cld  22594  indiscld  22595  neipeltop  22633  rest0  22673  restsn  22674  cmpfi  22912  refun0  23019  txindislem  23137  hmphindis  23301  xpstopnlem1  23313  xpstopnlem2  23315  ptcmpfi  23317  snfil  23368  fbasfip  23372  fgcl  23382  filconn  23387  fbasrn  23388  cfinfil  23397  csdfil  23398  supfil  23399  ufildr  23435  fin1aufil  23436  rnelfmlem  23456  fclsval  23512  tmdgsum  23599  tsmsfbas  23632  ust0  23724  ustn0  23725  0met  23872  xpsdsval  23887  minveclem3b  24945  tdeglem2  25579  deg1ldg  25610  deg1leb  25613  deg1val  25614  ulm0  25903  nosgnn0  27161  nodense  27195  nolt02o  27198  nogt01o  27199  nulsslt  27298  nulssgt  27299  bday1s  27332  made0  27368  precsexlem1  27653  precsexlem2  27654  uhgr0  28333  upgr0eop  28374  upgr0eopALT  28376  usgr0  28500  usgr0eop  28503  lfuhgr1v0e  28511  griedg0prc  28521  0grsubgr  28535  cplgr0  28682  0grrusgr  28836  clwwlk0on0  29345  0ewlk  29367  0wlkon  29373  0trlon  29377  0pthon  29380  0pthonv  29382  0conngr  29445  konigsberglem1  29505  konigsberglem2  29506  konigsberglem3  29507  wlkl0  29620  disjdifprg  31806  disjun0  31826  fpwrelmapffslem  31957  f1ocnt  32013  resvsca  32444  locfinref  32821  zarcmplem  32861  esumnul  33046  esumrnmpt2  33066  prsiga  33129  ldsysgenld  33158  ldgenpisyslem1  33161  oms0  33296  carsggect  33317  eulerpartgbij  33371  eulerpartlemmf  33374  repr0  33623  breprexp  33645  bnj941  33783  bnj97  33877  bnj149  33886  bnj150  33887  bnj944  33949  fineqvac  34097  derang0  34160  indispconn  34225  goeleq12bg  34340  satf0  34363  satf0op  34368  fmla0  34373  fmla0xp  34374  fmlasuc0  34375  fmlafvel  34376  fmlasuc  34377  fmlaomn0  34381  fmla0disjsuc  34389  satfdmfmla  34391  satfv0fvfmla0  34404  sate0  34406  sate0fv0  34408  sategoelfvb  34410  ex-sategoelel  34412  prv0  34421  prv1n  34422  rdgprc  34766  dfrdg3  34768  fullfunfnv  34918  fullfunfv  34919  rank0  35142  ssoninhaus  35333  onint1  35334  bj-0nel1  35834  bj-xpnzex  35840  bj-eltag  35858  bj-0eltag  35859  bj-tagss  35861  bj-pr1val  35885  bj-snex  35916  bj-snfromadj  35925  bj-nuliota  35938  bj-nuliotaALT  35939  bj-rdg0gALT  35952  bj-rest10  35969  bj-rest10b  35970  bj-rest0  35974  rdgssun  36259  finxpreclem1  36270  finxpreclem2  36271  finxp0  36272  finxpreclem5  36276  poimirlem28  36516  heibor1lem  36677  heiborlem6  36684  reheibor  36707  n0elqs  37195  sticksstones11  40972  mzpcompact2lem  41489  wopprc  41769  pw2f1ocnv  41776  pwslnmlem0  41833  pwfi2f1o  41838  2omomeqom  42053  cantnfub  42071  cantnfresb  42074  omcl3g  42084  nadd1suc  42142  naddwordnexlem4  42152  nla0002  42175  nla0003  42176  nla0001  42177  clsk1indlem0  42792  clsk1indlem4  42795  clsk1indlem1  42796  mnupwd  43026  mnuprdlem1  43031  mnuprdlem2  43032  mnuprdlem3  43033  mnurnd  43042  fnchoice  43713  eliuniincex  43798  limsup0  44410  0cnv  44458  liminf0  44509  0cnf  44593  dvnprodlem3  44664  qndenserrnbl  45011  prsal  45034  intsal  45046  sge00  45092  sge0sn  45095  nnfoctbdjlem  45171  isomenndlem  45246  hoiqssbl  45341  ovnsubadd2lem  45361  upwordnul  45594  iota0def  45748  aiota0def  45804  afv0fv0  45857  0nelsetpreimafv  46058  lincval0  47096  lco0  47108  linds0  47146  0aryfvalel  47320  0aryfvalelfv  47321  1aryenef  47331  2aryenef  47342  mof0  47504  0thinc  47671  setc2othin  47676  prstcthin  47696  bnd2d  47726