Theorem 0ex 5242

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

Syntax hints:  ¬ wn 3  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3430  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-nul 4275

This theorem is referenced by:  al0ssb  5243  sseliALT  5244  csbexg  5245  unisn2  5247  class2set  5292  0elpw  5293  0nep0  5295  unidif0  5297  iin0  5299  notzfaus  5300  intv  5301  snexALT  5320  p0ex  5321  dtruALT  5325  zfpair  5358  snexOLD  5379  opexOLD  5412  opthwiener  5462  0sn0ep  5528  opthprc  5688  nrelv  5749  dmsnsnsn  6178  0elon  6372  nsuceq0  6402  snsn0non  6443  iotaex  6468  fun0  6557  fvrn0  6862  fprg  7102  ovima0  7539  onint0  7738  tfinds2  7808  finds  7840  finds2  7842  xpexr  7862  soex  7865  supp0  8108  fvn0elsupp  8123  fvn0elsuppb  8124  brtpos0  8176  reldmtpos  8177  tfrlem16  8325  tz7.44-1  8338  seqomlem1  8382  1n0  8416  nlim1  8417  nlim2  8418  el1o  8423  om0  8445  mapdm0  8782  fsetexb  8804  0map0sn0  8826  ixpexg  8863  0elixp  8870  en0  8958  en0ALT  8959  en0r  8960  ensn1  8961  en1  8964  2dom  8970  map1  8980  enpr2d  8988  xp1en  8994  endisj  8995  pw2eng  9014  0domg  9035  map2xp  9078  limensuci  9084  snnen2o  9148  0sdom1dom  9149  rex2dom  9156  1sdom2dom  9157  unxpdom2  9163  sucxpdom  9164  isinf  9168  ac6sfi  9187  fodomfi  9215  fodomfiOLD  9233  0fsupp  9296  fi0  9326  oiexg  9443  brwdom  9475  brwdom2  9481  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  20967  cnfldfun  21358  cnfldfunOLD  21371  frgpcyg  21563  frlmiscvec  21839  fvcoe1  22181  coe1f2  22183  coe1sfi  22187  coe1add  22239  coe1mul2lem1  22242  coe1mul2lem2  22243  coe1mul2  22244  ply1coe  22273  evls1rhmlem  22296  evl1sca  22309  evl1var  22311  pf1mpf  22327  pf1ind  22330  mat0dimscm  22444  mat0dimcrng  22445  mat0scmat  22513  mavmul0  22527  mavmul0g  22528  mvmumamul1  22529  mdet0pr  22567  mdet0f1o  22568  mdet0fv0  22569  mdetunilem9  22595  d0mat2pmat  22713  chpmat0d  22809  en1top  22959  en2top  22960  sn0topon  22973  indistopon  22976  indistps  22986  indistps2  22987  sn0cld  23065  indiscld  23066  neipeltop  23104  rest0  23144  restsn  23145  cmpfi  23383  refun0  23490  txindislem  23608  hmphindis  23772  xpstopnlem1  23784  xpstopnlem2  23786  ptcmpfi  23788  snfil  23839  fbasfip  23843  fgcl  23853  filconn  23858  fbasrn  23859  cfinfil  23868  csdfil  23869  supfil  23870  ufildr  23906  fin1aufil  23907  rnelfmlem  23927  fclsval  23983  tmdgsum  24070  tsmsfbas  24103  ust0  24195  ustn0  24196  0met  24341  xpsdsval  24356  minveclem3b  25405  tdeglem2  26036  deg1ldg  26067  deg1leb  26070  deg1val  26071  ulm0  26369  nosgnn0  27636  nodense  27670  nolt02o  27673  nogt01o  27674  nulslts  27781  nulsgts  27782  bday1  27820  made0  27869  precsexlem1  28213  precsexlem2  28214  uhgr0  29156  upgr0eop  29197  upgr0eopALT  29199  usgr0  29326  usgr0eop  29329  lfuhgr1v0e  29337  griedg0prc  29347  0grsubgr  29361  cplgr0  29508  0grrusgr  29663  clwwlk0on0  30177  0ewlk  30199  0wlkon  30205  0trlon  30209  0pthon  30212  0pthonv  30214  0conngr  30277  konigsberglem1  30337  konigsberglem2  30338  konigsberglem3  30339  wlkl0  30452  disjdifprg  32660  disjun0  32680  of0r  32767  fpwrelmapffslem  32820  f1ocnt  32888  resvsca  33407  1arithidom  33612  vieta  33739  locfinref  34001  zarcmplem  34041  esumnul  34208  esumrnmpt2  34228  prsiga  34291  ldsysgenld  34320  ldgenpisyslem1  34323  oms0  34457  carsggect  34478  eulerpartgbij  34532  eulerpartlemmf  34535  repr0  34771  breprexp  34793  bnj941  34931  bnj97  35024  bnj149  35033  bnj150  35034  bnj944  35096  fineqvac  35276  fineqvnttrclse  35284  wevgblacfn  35307  derang0  35367  indispconn  35432  goeleq12bg  35547  satf0  35570  satf0op  35575  fmla0  35580  fmla0xp  35581  fmlasuc0  35582  fmlafvel  35583  fmlasuc  35584  fmlaomn0  35588  fmla0disjsuc  35596  satfdmfmla  35598  satfv0fvfmla0  35611  sate0  35613  sate0fv0  35615  sategoelfvb  35617  ex-sategoelel  35619  prv0  35628  prv1n  35629  rdgprc  35990  dfrdg3  35992  fullfunfnv  36144  fullfunfv  36145  rank0  36368  ssoninhaus  36646  onint1  36647  mh-infprim2bi  36745  bj-0nel1  37276  bj-xpnzex  37282  bj-eltag  37300  bj-0eltag  37301  bj-tagss  37303  bj-pr1val  37327  bj-snex  37358  bj-snfromadj  37367  bj-nuliota  37380  bj-nuliotaALT  37381  bj-rdg0gALT  37394  bj-rest10  37416  bj-rest10b  37417  bj-rest0  37421  rdgssun  37708  finxpreclem1  37719  finxpreclem2  37720  finxp0  37721  finxpreclem5  37725  poimirlem28  37983  heibor1lem  38144  heiborlem6  38151  reheibor  38174  n0elqs  38667  sticksstones11  42609  mzpcompact2lem  43197  wopprc  43476  pw2f1ocnv  43483  pwslnmlem0  43537  pwfi2f1o  43542  2omomeqom  43749  cantnfub  43767  cantnfresb  43770  omcl3g  43780  nadd1suc  43838  naddwordnexlem4  43847  nla0002  43869  nla0003  43870  nla0001  43871  clsk1indlem0  44486  clsk1indlem4  44489  clsk1indlem1  44490  mnupwd  44712  mnuprdlem1  44717  mnuprdlem2  44718  mnuprdlem3  44719  mnurnd  44728  permaxnul  45453  permaxinf2lem  45457  nregmodelf1o  45460  nregmodellem  45461  nregmodel  45462  fnchoice  45478  eliuniincex  45557  limsup0  46140  0cnv  46188  liminf0  46239  0cnf  46323  dvnprodlem3  46394  qndenserrnbl  46741  prsal  46764  intsal  46776  sge00  46822  sge0sn  46825  nnfoctbdjlem  46901  isomenndlem  46976  hoiqssbl  47071  ovnsubadd2lem  47091  iota0def  47498  aiota0def  47556  afv0fv0  47609  0nelsetpreimafv  47862  lincval0  48903  lco0  48915  linds0  48953  0aryfvalel  49122  0aryfvalelfv  49123  1aryenef  49133  2aryenef  49144  mof0  49325  dftpos5  49361  dftpos6  49362  relcic  49532  discsubclem  49550  discsubc  49551  iinfconstbas  49553  nelsubclem  49554  0funcg  49572  0func  49574  0funcALT  49575  oppffn  49611  oppfvalg  49613  fucofvalne  49812  0thinc  49946  setc2othin  49953  setc1ohomfval  49980  setc1ocofval  49981  isinito2lem  49985  prstcthin  50048  setc1onsubc  50089  initocmd  50156  termolmd  50157  bnd2d  50168