Theorem 0ex 5269

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

Syntax hints:  ¬ wn 3  ∀wal 1565   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3463  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-nul 4295

This theorem is referenced by:  al0ssb  5270  sseliALT  5271  csbexg  5272  unisn2  5274  class2set  5323  0elpw  5324  0nep0  5326  unidif0  5328  unidif0OLD  5329  iin0  5331  notzfaus  5332  intv  5333  snexALT  5352  p0ex  5353  dtruALT  5357  zfpair  5390  snexOLD  5411  opexOLD  5444  opthwiener  5495  0sn0ep  5563  opthprc  5723  nrelv  5784  nrelvOLD  5785  dmsnsnsn  6218  0elon  6413  nsuceq0  6443  snsn0non  6484  iotaex  6509  fun0  6598  fvrn0  6907  fprg  7150  ovima0  7587  onint0  7786  tfinds2  7856  finds  7889  finds2  7891  xpexr  7911  soex  7914  supp0  8157  fvn0elsupp  8172  fvn0elsuppb  8173  brtpos0  8225  reldmtpos  8226  tfrlem16  8376  tz7.44-1  8389  seqomlem1  8433  1n0OLD  8469  nlim1  8470  nlim2  8471  el1o  8476  om0  8498  mapdm0  8835  fsetexb  8857  0map0sn0  8879  ixpexg  8916  0elixp  8923  en0  9011  en0ALT  9012  en0r  9013  ensn1  9014  en1  9017  2dom  9023  map1  9033  enpr2d  9041  xp1en  9047  endisj  9048  pw2eng  9067  0domg  9088  map2xp  9131  limensuci  9137  snnen2o  9201  0sdom1dom  9202  rex2dom  9209  1sdom2dom  9210  unxpdom2  9216  sucxpdom  9217  isinf  9221  ac6sfi  9240  fodomfi  9268  0fsupp  9346  fi0  9376  oiexg  9493  brwdom  9525  brwdom2  9531  inf3lemb  9590  infeq5i  9601  dfom3  9612  cantnfvalf  9630  cantnfval2  9634  cantnfle  9636  cantnflt  9637  cantnff  9639  cantnf0  9640  cantnfp1lem1  9643  cantnfp1lem3  9645  cantnfp1  9646  cantnflem1a  9650  cantnflem1d  9653  cantnflem1  9654  cantnf  9658  cnfcomlem  9664  cnfcom  9665  cnfcom2lem  9666  cnfcom3  9669  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  dmttrcl  9686  ttrclselem2  9691  tc0  9710  r10  9736  scottex  9855  djulcl  9892  djulf1o  9894  djuss  9902  djuun  9908  1stinl  9909  2ndinl  9910  infxpenlem  9993  fseqenlem1  10004  undjudom  10147  endjudisj  10148  djuen  10149  dju1dif  10152  dju1p1e2  10153  dju0en  10155  djucomen  10157  djuassen  10158  xpdjuen  10159  mapdjuen  10160  djuxpdom  10165  djuinf  10168  infdju1  10169  djulepw  10172  pwsdompw  10182  pwdjudom  10194  ackbij1lem14  10211  ackbij2lem2  10218  ackbij2lem3  10219  cf0  10230  cfeq0  10236  cfsuc  10237  cflim2  10243  isfin5  10279  isfin4p1  10295  fin1a2lem11  10390  fin1a2lem12  10391  fin1a2lem13  10392  axcc2lem  10416  ac6num  10459  zornn0g  10485  ttukeylem3  10491  brdom3  10508  iundom2g  10520  cardeq0  10532  pwcfsdom  10564  axpowndlem3  10580  canthwe  10632  canthp1lem1  10633  pwxpndom2  10646  pwdjundom  10648  gchxpidm  10650  intwun  10716  0tsk  10736  grothomex  10810  indpi  10888  fzennn  14000  hash0  14399  hashen1  14402  hashmap  14468  hashbc  14486  hashf1  14490  hashge3el3dif  14520  ccat1st1st  14662  swrdval  14677  swrd00  14678  swrd0  14692  cshfn  14823  cshnz  14825  0csh0  14826  incexclem  15886  incexc  15887  rexpen  16280  sadcf  16507  sadc0  16508  sadcp1  16509  smupf  16532  smup0  16533  smupp1  16534  0ram  17076  ram0  17078  cshws0  17157  str0  17245  ress0  17299  0rest  17478  fnpr2ob  17608  xpsfrnel  17612  xpsle  17629  ismred2  17651  acsfn  17711  0cat  17741  ciclcl  17855  cicrcl  17856  cicer  17859  setcepi  18141  setc2obas  18147  setc2ohom  18148  cat1  18150  0pos  18373  join0  18455  meet0  18456  mgm0b  18711  gsum0  18738  sgrp0b  18782  efmnd0nmnd  18945  pwmnd  18995  mulgfval  19131  ga0  19364  psgn0fv0  19577  pmtrsn  19585  oppglsm  19708  efgi0  19786  vrgpf  19834  vrgpinv  19835  frgpuptinv  19837  frgpup2  19842  0frgp  19845  frgpnabllem1  19939  frgpnabllem2  19940  dprd0  20099  dmdprdpr  20117  dprdpr  20118  00lsp  21076  cnfldfun  21501  frgpcyg  21688  frlmiscvec  21964  fvcoe1  22332  coe1f2  22334  coe1sfi  22338  coe1add  22390  coe1mul2lem1  22393  coe1mul2lem2  22394  coe1mul2  22395  ply1coe  22423  evls1rhmlem  22446  evl1sca  22459  evl1var  22461  pf1mpf  22477  pf1ind  22480  mat0dimscm  22591  mat0dimcrng  22592  mat0scmat  22660  mavmul0  22674  mavmul0g  22675  mvmumamul1  22676  mdet0pr  22714  mdet0f1o  22715  mdet0fv0  22716  mdetunilem9  22742  d0mat2pmat  22860  chpmat0d  22956  en1top  23106  en2top  23107  sn0topon  23120  indistopon  23123  indistps  23133  indistps2  23134  sn0cld  23212  indiscld  23213  neipeltop  23251  rest0  23291  restsn  23292  cmpfi  23530  refun0  23637  txindislem  23755  hmphindis  23919  xpstopnlem1  23931  xpstopnlem2  23933  ptcmpfi  23935  snfil  23986  fbasfip  23990  fgcl  24000  filconn  24005  fbasrn  24006  cfinfil  24015  csdfil  24016  supfil  24017  ufildr  24053  fin1aufil  24054  rnelfmlem  24074  fclsval  24130  tmdgsum  24217  tsmsfbas  24250  ust0  24342  ustn0  24343  0met  24488  xpsdsval  24503  minveclem3b  25552  tdeglem2  26183  deg1ldg  26214  deg1leb  26217  deg1val  26218  ulm0  26516  nosgnn0  27784  nodense  27818  nolt02o  27821  nogt01o  27822  nulslts  27930  nulsgts  27931  bday1  27969  made0  28018  precsexlem1  28362  precsexlem2  28363  uhgr0  29360  upgr0eop  29401  upgr0eopALT  29403  usgr0  29530  usgr0eop  29533  lfuhgr1v0e  29541  griedg0prc  29551  0grsubgr  29565  cplgr0  29712  0grrusgr  29866  clwwlk0on0  30380  0ewlk  30402  0wlkon  30408  0trlon  30412  0pthon  30415  0pthonv  30417  0conngr  30480  konigsberglem1  30540  konigsberglem2  30541  konigsberglem3  30542  wlkl0  30655  disjdifprg  32857  disjun0  32877  of0r  32961  fpwrelmapffslem  33014  f1ocnt  33082  resvsca  33591  1arithidom  33768  0mplrim  33845  selvply1rhmlema  33849  selvply1rhmlemb  33850  selvply1rhmlem1  33851  selvply1rhm0  33857  mplidomlem  33858  vieta  33911  locfinref  34172  zarcmplem  34212  esumnul  34379  esumrnmpt2  34399  prsiga  34462  ldsysgenld  34491  ldgenpisyslem1  34494  oms0  34628  carsggect  34649  eulerpartgbij  34703  eulerpartlemmf  34706  repr0  34939  breprexp  34961  bnj941  35102  bnj97  35195  bnj149  35204  bnj150  35205  bnj944  35267  fineqvac  35448  fineqvnttrclse  35456  wevgblacfn  35490  derang0  35556  indispconn  35621  goeleq12bg  35736  satf0  35759  satf0op  35764  fmla0  35769  fmla0xp  35770  fmlasuc0  35771  fmlafvel  35772  fmlasuc  35773  fmlaomn0  35777  fmla0disjsuc  35785  satfdmfmla  35787  satfv0fvfmla0  35800  sate0  35802  sate0fv0  35804  sategoelfvb  35806  ex-sategoelel  35808  prv0  35817  prv1n  35818  rdgprc  36179  dfrdg3  36181  fullfunfnv  36333  fullfunfv  36334  rank0  36557  ssoninhaus  36844  onint1  36845  mh-infprim2bi  36943  bj-0nel1  37473  bj-xpnzex  37479  bj-eltag  37497  bj-0eltag  37498  bj-tagss  37500  bj-pr1val  37524  bj-snex  37555  bj-snfromadj  37564  bj-nuliota  37577  bj-nuliotaALT  37578  bj-rdg0gALT  37591  bj-rest10  37613  bj-rest10b  37614  bj-rest0  37618  rdgssun  37907  finxpreclem1  37918  finxpreclem2  37919  finxp0  37920  finxpreclem5  37924  poimirlem28  38182  heibor1lem  38343  heiborlem6  38350  reheibor  38373  n0elqs  38866  sticksstones11  42808  mzpcompact2lem  43367  wopprc  43642  pw2f1ocnv  43649  pwslnmlem0  43703  pwfi2f1o  43708  2omomeqom  43915  cantnfub  43933  cantnfresb  43936  omcl3g  43946  nadd1suc  44004  naddwordnexlem4  44013  nla0002  44035  nla0003  44036  nla0001  44037  clsk1indlem0  44652  clsk1indlem4  44655  clsk1indlem1  44656  mnupwd  44862  mnuprdlem1  44867  mnuprdlem2  44868  mnuprdlem3  44869  mnurnd  44878  permaxnul  45602  permaxinf2lem  45606  nregmodelf1o  45609  nregmodellem  45610  nregmodel  45611  fnchoice  45634  eliuniincex  45712  limsup0  46293  0cnv  46341  liminf0  46392  0cnf  46476  dvnprodlem3  46547  qndenserrnbl  46894  prsal  46917  intsal  46929  sge00  46975  sge0sn  46978  nnfoctbdjlem  47054  isomenndlem  47129  hoiqssbl  47224  ovnsubadd2lem  47244  iota0def  47657  aiota0def  47715  afv0fv0  47768  0nelsetpreimafv  48021  lincval0  49073  lco0  49085  linds0  49123  0aryfvalel  49292  0aryfvalelfv  49293  1aryenef  49303  2aryenef  49314  mof0  49494  dftpos5  49530  dftpos6  49531  relcic  49701  discsubclem  49719  discsubc  49720  iinfconstbas  49722  nelsubclem  49723  0funcg  49741  0func  49743  0funcALT  49744  oppffn  49780  oppfvalg  49782  fucofvalne  49981  0thinc  50115  setc2othin  50122  setc1ohomfval  50149  setc1ocofval  50150  isinito2lem  50154  prstcthin  50217  setc1onsubc  50258  initocmd  50325  termolmd  50326  bnd2d  50337