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

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

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-nul 4274

This theorem is referenced by:  al0ssb  5243  sseliALT  5244  csbexg  5245  unisn2  5247  class2set  5296  0elpw  5297  0nep0  5299  unidif0  5301  unidif0OLD  5302  iin0  5304  notzfaus  5305  intv  5306  snexALT  5325  p0ex  5326  dtruALT  5330  zfpair  5363  snexOLD  5384  opexOLD  5417  opthwiener  5468  0sn0ep  5535  opthprc  5695  nrelv  5756  dmsnsnsn  6184  0elon  6378  nsuceq0  6408  snsn0non  6449  iotaex  6474  fun0  6563  fvrn0  6868  fprg  7109  ovima0  7546  onint0  7745  tfinds2  7815  finds  7847  finds2  7849  xpexr  7869  soex  7872  supp0  8115  fvn0elsupp  8130  fvn0elsuppb  8131  brtpos0  8183  reldmtpos  8184  tfrlem16  8332  tz7.44-1  8345  seqomlem1  8389  1n0  8423  nlim1  8424  nlim2  8425  el1o  8430  om0  8452  mapdm0  8789  fsetexb  8811  0map0sn0  8833  ixpexg  8870  0elixp  8877  en0  8965  en0ALT  8966  en0r  8967  ensn1  8968  en1  8971  2dom  8977  map1  8987  enpr2d  8995  xp1en  9001  endisj  9002  pw2eng  9021  0domg  9042  map2xp  9085  limensuci  9091  snnen2o  9155  0sdom1dom  9156  rex2dom  9163  1sdom2dom  9164  unxpdom2  9170  sucxpdom  9171  isinf  9175  ac6sfi  9194  fodomfi  9222  fodomfiOLD  9240  0fsupp  9303  fi0  9333  oiexg  9450  brwdom  9482  brwdom2  9488  inf3lemb  9546  infeq5i  9557  dfom3  9568  cantnfvalf  9586  cantnfval2  9590  cantnfle  9592  cantnflt  9593  cantnff  9595  cantnf0  9596  cantnfp1lem1  9599  cantnfp1lem3  9601  cantnfp1  9602  cantnflem1a  9606  cantnflem1d  9609  cantnflem1  9610  cantnf  9614  cnfcomlem  9620  cnfcom  9621  cnfcom2lem  9622  cnfcom3  9625  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  dmttrcl  9642  ttrclselem2  9647  tc0  9666  r10  9692  scottex  9809  djulcl  9834  djulf1o  9836  djuss  9844  djuun  9850  1stinl  9851  2ndinl  9852  infxpenlem  9935  fseqenlem1  9946  undjudom  10090  endjudisj  10091  djuen  10092  dju1dif  10095  dju1p1e2  10096  dju0en  10098  djucomen  10100  djuassen  10101  xpdjuen  10102  mapdjuen  10103  djuxpdom  10108  djuinf  10111  infdju1  10112  djulepw  10115  pwsdompw  10125  pwdjudom  10137  ackbij1lem14  10154  ackbij2lem2  10161  ackbij2lem3  10162  cf0  10173  cfeq0  10178  cfsuc  10179  cflim2  10185  isfin5  10221  isfin4p1  10237  fin1a2lem11  10332  fin1a2lem12  10333  fin1a2lem13  10334  axcc2lem  10358  ac6num  10401  zornn0g  10427  ttukeylem3  10433  brdom3  10450  iundom2g  10462  cardeq0  10474  pwcfsdom  10506  axpowndlem3  10522  canthwe  10574  canthp1lem1  10575  pwxpndom2  10588  pwdjundom  10590  gchxpidm  10592  intwun  10658  0tsk  10678  grothomex  10752  indpi  10830  fzennn  13930  hash0  14329  hashen1  14332  hashmap  14397  hashbc  14415  hashf1  14419  hashge3el3dif  14449  ccat1st1st  14591  swrdval  14606  swrd00  14607  swrd0  14621  cshfn  14752  cshnz  14754  0csh0  14755  incexclem  15801  incexc  15802  rexpen  16195  sadcf  16422  sadc0  16423  sadcp1  16424  smupf  16447  smup0  16448  smupp1  16449  0ram  16991  ram0  16993  cshws0  17072  str0  17159  ress0  17213  0rest  17392  fnpr2ob  17522  xpsfrnel  17526  xpsle  17543  ismred2  17565  acsfn  17625  0cat  17655  ciclcl  17769  cicrcl  17770  cicer  17773  setcepi  18055  setc2obas  18061  setc2ohom  18062  cat1  18064  0pos  18287  join0  18369  meet0  18370  mgm0b  18625  gsum0  18652  sgrp0b  18696  efmnd0nmnd  18858  pwmnd  18908  mulgfval  19045  ga0  19273  psgn0fv0  19486  pmtrsn  19494  oppglsm  19617  efgi0  19695  vrgpf  19743  vrgpinv  19744  frgpuptinv  19746  frgpup2  19751  0frgp  19754  frgpnabllem1  19848  frgpnabllem2  19849  dprd0  20008  dmdprdpr  20026  dprdpr  20027  00lsp  20976  cnfldfun  21366  frgpcyg  21553  frlmiscvec  21829  fvcoe1  22171  coe1f2  22173  coe1sfi  22177  coe1add  22229  coe1mul2lem1  22232  coe1mul2lem2  22233  coe1mul2  22234  ply1coe  22263  evls1rhmlem  22286  evl1sca  22299  evl1var  22301  pf1mpf  22317  pf1ind  22320  mat0dimscm  22434  mat0dimcrng  22435  mat0scmat  22503  mavmul0  22517  mavmul0g  22518  mvmumamul1  22519  mdet0pr  22557  mdet0f1o  22558  mdet0fv0  22559  mdetunilem9  22585  d0mat2pmat  22703  chpmat0d  22799  en1top  22949  en2top  22950  sn0topon  22963  indistopon  22966  indistps  22976  indistps2  22977  sn0cld  23055  indiscld  23056  neipeltop  23094  rest0  23134  restsn  23135  cmpfi  23373  refun0  23480  txindislem  23598  hmphindis  23762  xpstopnlem1  23774  xpstopnlem2  23776  ptcmpfi  23778  snfil  23829  fbasfip  23833  fgcl  23843  filconn  23848  fbasrn  23849  cfinfil  23858  csdfil  23859  supfil  23860  ufildr  23896  fin1aufil  23897  rnelfmlem  23917  fclsval  23973  tmdgsum  24060  tsmsfbas  24093  ust0  24185  ustn0  24186  0met  24331  xpsdsval  24346  minveclem3b  25395  tdeglem2  26026  deg1ldg  26057  deg1leb  26060  deg1val  26061  ulm0  26356  nosgnn0  27622  nodense  27656  nolt02o  27659  nogt01o  27660  nulslts  27767  nulsgts  27768  bday1  27806  made0  27855  precsexlem1  28199  precsexlem2  28200  uhgr0  29142  upgr0eop  29183  upgr0eopALT  29185  usgr0  29312  usgr0eop  29315  lfuhgr1v0e  29323  griedg0prc  29333  0grsubgr  29347  cplgr0  29494  0grrusgr  29648  clwwlk0on0  30162  0ewlk  30184  0wlkon  30190  0trlon  30194  0pthon  30197  0pthonv  30199  0conngr  30262  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  wlkl0  30437  disjdifprg  32645  disjun0  32665  of0r  32752  fpwrelmapffslem  32805  f1ocnt  32873  resvsca  33392  1arithidom  33597  vieta  33724  locfinref  33985  zarcmplem  34025  esumnul  34192  esumrnmpt2  34212  prsiga  34275  ldsysgenld  34304  ldgenpisyslem1  34307  oms0  34441  carsggect  34462  eulerpartgbij  34516  eulerpartlemmf  34519  repr0  34755  breprexp  34777  bnj941  34915  bnj97  35008  bnj149  35017  bnj150  35018  bnj944  35080  fineqvac  35260  fineqvnttrclse  35268  wevgblacfn  35291  derang0  35351  indispconn  35416  goeleq12bg  35531  satf0  35554  satf0op  35559  fmla0  35564  fmla0xp  35565  fmlasuc0  35566  fmlafvel  35567  fmlasuc  35568  fmlaomn0  35572  fmla0disjsuc  35580  satfdmfmla  35582  satfv0fvfmla0  35595  sate0  35597  sate0fv0  35599  sategoelfvb  35601  ex-sategoelel  35603  prv0  35612  prv1n  35613  rdgprc  35974  dfrdg3  35976  fullfunfnv  36128  fullfunfv  36129  rank0  36352  ssoninhaus  36630  onint1  36631  mh-infprim2bi  36729  bj-0nel1  37260  bj-xpnzex  37266  bj-eltag  37284  bj-0eltag  37285  bj-tagss  37287  bj-pr1val  37311  bj-snex  37342  bj-snfromadj  37351  bj-nuliota  37364  bj-nuliotaALT  37365  bj-rdg0gALT  37378  bj-rest10  37400  bj-rest10b  37401  bj-rest0  37405  rdgssun  37694  finxpreclem1  37705  finxpreclem2  37706  finxp0  37707  finxpreclem5  37711  poimirlem28  37969  heibor1lem  38130  heiborlem6  38137  reheibor  38160  n0elqs  38653  sticksstones11  42595  mzpcompact2lem  43183  wopprc  43458  pw2f1ocnv  43465  pwslnmlem0  43519  pwfi2f1o  43524  2omomeqom  43731  cantnfub  43749  cantnfresb  43752  omcl3g  43762  nadd1suc  43820  naddwordnexlem4  43829  nla0002  43851  nla0003  43852  nla0001  43853  clsk1indlem0  44468  clsk1indlem4  44471  clsk1indlem1  44472  mnupwd  44694  mnuprdlem1  44699  mnuprdlem2  44700  mnuprdlem3  44701  mnurnd  44710  permaxnul  45435  permaxinf2lem  45439  nregmodelf1o  45442  nregmodellem  45443  nregmodel  45444  fnchoice  45460  eliuniincex  45539  limsup0  46122  0cnv  46170  liminf0  46221  0cnf  46305  dvnprodlem3  46376  qndenserrnbl  46723  prsal  46746  intsal  46758  sge00  46804  sge0sn  46807  nnfoctbdjlem  46883  isomenndlem  46958  hoiqssbl  47053  ovnsubadd2lem  47073  iota0def  47486  aiota0def  47544  afv0fv0  47597  0nelsetpreimafv  47850  lincval0  48891  lco0  48903  linds0  48941  0aryfvalel  49110  0aryfvalelfv  49111  1aryenef  49121  2aryenef  49132  mof0  49313  dftpos5  49349  dftpos6  49350  relcic  49520  discsubclem  49538  discsubc  49539  iinfconstbas  49541  nelsubclem  49542  0funcg  49560  0func  49562  0funcALT  49563  oppffn  49599  oppfvalg  49601  fucofvalne  49800  0thinc  49934  setc2othin  49941  setc1ohomfval  49968  setc1ocofval  49969  isinito2lem  49973  prstcthin  50036  setc1onsubc  50077  initocmd  50144  termolmd  50145  bnd2d  50156