Theorem 0ex 5249

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

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

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 5248

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 3440  df-dif 3908  df-nul 4287

This theorem is referenced by:  al0ssb  5250  sseliALT  5251  csbexg  5252  unisn2  5254  class2set  5297  0elpw  5298  0nep0  5300  unidif0  5302  iin0  5304  notzfaus  5305  intv  5306  snexALT  5325  p0ex  5326  dtruALT  5330  zfpair  5363  snex  5378  opex  5411  opthwiener  5461  0sn0ep  5527  opthprc  5687  nrelv  5747  dmsnsnsn  6173  0elon  6366  nsuceq0  6396  snsn0non  6437  iotaex  6462  fun0  6551  fvrn0  6854  fvssunirnOLD  6858  fprg  7093  ovima0  7532  onint0  7731  tfinds2  7804  finds  7836  finds2  7838  xpexr  7858  soex  7861  supp0  8105  fvn0elsupp  8120  fvn0elsuppb  8121  brtpos0  8173  reldmtpos  8174  tfrlem16  8322  tz7.44-1  8335  seqomlem1  8379  1n0  8413  nlim1  8414  nlim2  8415  el1o  8420  om0  8442  mapdm0  8776  fsetexb  8798  0map0sn0  8819  ixpexg  8856  0elixp  8863  en0  8950  en0ALT  8951  en0r  8952  ensn1  8953  en1  8956  2dom  8962  map1  8972  enpr2d  8981  xp1en  8987  endisj  8988  pw2eng  9007  0domg  9028  map2xp  9071  limensuci  9077  snnen2o  9144  0sdom1dom  9145  rex2dom  9152  1sdom2dom  9153  unxpdom2  9159  sucxpdom  9160  isinf  9165  isinfOLD  9166  ac6sfi  9189  fodomfi  9219  fodomfiOLD  9239  0fsupp  9299  fi0  9329  oiexg  9446  brwdom  9478  brwdom2  9484  inf3lemb  9540  infeq5i  9551  dfom3  9562  cantnfvalf  9580  cantnfval2  9584  cantnfle  9586  cantnflt  9587  cantnff  9589  cantnf0  9590  cantnfp1lem1  9593  cantnfp1lem3  9595  cantnfp1  9596  cantnflem1a  9600  cantnflem1d  9603  cantnflem1  9604  cantnf  9608  cnfcomlem  9614  cnfcom  9615  cnfcom2lem  9616  cnfcom3  9619  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  dmttrcl  9636  ttrclselem2  9641  tc0  9662  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  10496  axpowndlem3  10512  canthwe  10564  canthp1lem1  10565  pwxpndom2  10578  pwdjundom  10580  gchxpidm  10582  intwun  10648  0tsk  10668  grothomex  10742  indpi  10820  fzennn  13893  hash0  14292  hashen1  14295  hashmap  14360  hashbc  14378  hashf1  14382  hashge3el3dif  14412  ccat1st1st  14553  swrdval  14568  swrd00  14569  swrd0  14583  cshfn  14714  cshnz  14716  0csh0  14717  incexclem  15761  incexc  15762  rexpen  16155  sadcf  16382  sadc0  16383  sadcp1  16384  smupf  16407  smup0  16408  smupp1  16409  0ram  16950  ram0  16952  cshws0  17031  str0  17118  ress0  17172  0rest  17351  fnpr2ob  17480  xpsfrnel  17484  xpsle  17501  ismred2  17523  acsfn  17583  0cat  17613  ciclcl  17727  cicrcl  17728  cicer  17731  setcepi  18013  setc2obas  18019  setc2ohom  18020  cat1  18022  0pos  18245  join0  18327  meet0  18328  mgm0b  18549  gsum0  18576  sgrp0b  18620  efmnd0nmnd  18782  pwmnd  18829  mulgfval  18966  ga0  19195  psgn0fv0  19408  pmtrsn  19416  oppglsm  19539  efgi0  19617  vrgpf  19665  vrgpinv  19666  frgpuptinv  19668  frgpup2  19673  0frgp  19676  frgpnabllem1  19770  frgpnabllem2  19771  dprd0  19930  dmdprdpr  19948  dprdpr  19949  00lsp  20902  cnfldfun  21293  cnfldfunOLD  21306  frgpcyg  21498  frlmiscvec  21774  fvcoe1  22108  coe1f2  22110  coe1sfi  22114  coe1add  22166  coe1mul2lem1  22169  coe1mul2lem2  22170  coe1mul2  22171  ply1coe  22201  evls1rhmlem  22224  evl1sca  22237  evl1var  22239  pf1mpf  22255  pf1ind  22258  mat0dimscm  22372  mat0dimcrng  22373  mat0scmat  22441  mavmul0  22455  mavmul0g  22456  mvmumamul1  22457  mdet0pr  22495  mdet0f1o  22496  mdet0fv0  22497  mdetunilem9  22523  d0mat2pmat  22641  chpmat0d  22737  en1top  22887  en2top  22888  sn0topon  22901  indistopon  22904  indistps  22914  indistps2  22915  sn0cld  22993  indiscld  22994  neipeltop  23032  rest0  23072  restsn  23073  cmpfi  23311  refun0  23418  txindislem  23536  hmphindis  23700  xpstopnlem1  23712  xpstopnlem2  23714  ptcmpfi  23716  snfil  23767  fbasfip  23771  fgcl  23781  filconn  23786  fbasrn  23787  cfinfil  23796  csdfil  23797  supfil  23798  ufildr  23834  fin1aufil  23835  rnelfmlem  23855  fclsval  23911  tmdgsum  23998  tsmsfbas  24031  ust0  24123  ustn0  24124  0met  24270  xpsdsval  24285  minveclem3b  25344  tdeglem2  25982  deg1ldg  26013  deg1leb  26016  deg1val  26017  ulm0  26316  nosgnn0  27586  nodense  27620  nolt02o  27623  nogt01o  27624  nulsslt  27726  nulssgt  27727  bday1s  27763  made0  27805  precsexlem1  28132  precsexlem2  28133  uhgr0  29036  upgr0eop  29077  upgr0eopALT  29079  usgr0  29206  usgr0eop  29209  lfuhgr1v0e  29217  griedg0prc  29227  0grsubgr  29241  cplgr0  29388  0grrusgr  29543  clwwlk0on0  30054  0ewlk  30076  0wlkon  30082  0trlon  30086  0pthon  30089  0pthonv  30091  0conngr  30154  konigsberglem1  30214  konigsberglem2  30215  konigsberglem3  30216  wlkl0  30329  disjdifprg  32537  disjun0  32557  of0r  32635  fpwrelmapffslem  32688  f1ocnt  32758  resvsca  33283  1arithidom  33487  locfinref  33810  zarcmplem  33850  esumnul  34017  esumrnmpt2  34037  prsiga  34100  ldsysgenld  34129  ldgenpisyslem1  34132  oms0  34267  carsggect  34288  eulerpartgbij  34342  eulerpartlemmf  34345  repr0  34581  breprexp  34603  bnj941  34741  bnj97  34835  bnj149  34844  bnj150  34845  bnj944  34907  fineqvac  35074  wevgblacfn  35084  derang0  35144  indispconn  35209  goeleq12bg  35324  satf0  35347  satf0op  35352  fmla0  35357  fmla0xp  35358  fmlasuc0  35359  fmlafvel  35360  fmlasuc  35361  fmlaomn0  35365  fmla0disjsuc  35373  satfdmfmla  35375  satfv0fvfmla0  35388  sate0  35390  sate0fv0  35392  sategoelfvb  35394  ex-sategoelel  35396  prv0  35405  prv1n  35406  rdgprc  35770  dfrdg3  35772  fullfunfnv  35922  fullfunfv  35923  rank0  36146  ssoninhaus  36424  onint1  36425  bj-0nel1  36929  bj-xpnzex  36935  bj-eltag  36953  bj-0eltag  36954  bj-tagss  36956  bj-pr1val  36980  bj-snex  37011  bj-snfromadj  37020  bj-nuliota  37033  bj-nuliotaALT  37034  bj-rdg0gALT  37047  bj-rest10  37064  bj-rest10b  37065  bj-rest0  37069  rdgssun  37354  finxpreclem1  37365  finxpreclem2  37366  finxp0  37367  finxpreclem5  37371  poimirlem28  37630  heibor1lem  37791  heiborlem6  37798  reheibor  37821  n0elqs  38302  sticksstones11  42132  mzpcompact2lem  42727  wopprc  43006  pw2f1ocnv  43013  pwslnmlem0  43067  pwfi2f1o  43072  2omomeqom  43279  cantnfub  43297  cantnfresb  43300  omcl3g  43310  nadd1suc  43368  naddwordnexlem4  43377  nla0002  43400  nla0003  43401  nla0001  43402  clsk1indlem0  44017  clsk1indlem4  44020  clsk1indlem1  44021  mnupwd  44243  mnuprdlem1  44248  mnuprdlem2  44249  mnuprdlem3  44250  mnurnd  44259  permaxnul  44985  permaxinf2lem  44989  nregmodelf1o  44992  nregmodellem  44993  nregmodel  44994  fnchoice  45010  eliuniincex  45090  limsup0  45679  0cnv  45727  liminf0  45778  0cnf  45862  dvnprodlem3  45933  qndenserrnbl  46280  prsal  46303  intsal  46315  sge00  46361  sge0sn  46364  nnfoctbdjlem  46440  isomenndlem  46515  hoiqssbl  46610  ovnsubadd2lem  46630  upwordnul  46865  iota0def  47026  aiota0def  47084  afv0fv0  47137  0nelsetpreimafv  47378  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