Theorem 0ex 5254

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

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

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 5253

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 3444  df-dif 3906  df-nul 4288

This theorem is referenced by:  al0ssb  5255  sseliALT  5256  csbexg  5257  unisn2  5259  class2set  5302  0elpw  5303  0nep0  5305  unidif0  5307  iin0  5309  notzfaus  5310  intv  5311  snexALT  5330  p0ex  5331  dtruALT  5335  zfpair  5368  snexOLD  5388  opexOLD  5420  opthwiener  5470  0sn0ep  5536  opthprc  5696  nrelv  5757  dmsnsnsn  6186  0elon  6380  nsuceq0  6410  snsn0non  6451  iotaex  6476  fun0  6565  fvrn0  6870  fprg  7110  ovima0  7547  onint0  7746  tfinds2  7816  finds  7848  finds2  7850  xpexr  7870  soex  7873  supp0  8117  fvn0elsupp  8132  fvn0elsuppb  8133  brtpos0  8185  reldmtpos  8186  tfrlem16  8334  tz7.44-1  8347  seqomlem1  8391  1n0  8425  nlim1  8426  nlim2  8427  el1o  8432  om0  8454  mapdm0  8791  fsetexb  8813  0map0sn0  8835  ixpexg  8872  0elixp  8879  en0  8967  en0ALT  8968  en0r  8969  ensn1  8970  en1  8973  2dom  8979  map1  8989  enpr2d  8997  xp1en  9003  endisj  9004  pw2eng  9023  0domg  9044  map2xp  9087  limensuci  9093  snnen2o  9157  0sdom1dom  9158  rex2dom  9165  1sdom2dom  9166  unxpdom2  9172  sucxpdom  9173  isinf  9177  ac6sfi  9196  fodomfi  9224  fodomfiOLD  9242  0fsupp  9305  fi0  9335  oiexg  9452  brwdom  9484  brwdom2  9490  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  13903  hash0  14302  hashen1  14305  hashmap  14370  hashbc  14388  hashf1  14392  hashge3el3dif  14422  ccat1st1st  14564  swrdval  14579  swrd00  14580  swrd0  14594  cshfn  14725  cshnz  14727  0csh0  14728  incexclem  15771  incexc  15772  rexpen  16165  sadcf  16392  sadc0  16393  sadcp1  16394  smupf  16417  smup0  16418  smupp1  16419  0ram  16960  ram0  16962  cshws0  17041  str0  17128  ress0  17182  0rest  17361  fnpr2ob  17491  xpsfrnel  17495  xpsle  17512  ismred2  17534  acsfn  17594  0cat  17624  ciclcl  17738  cicrcl  17739  cicer  17742  setcepi  18024  setc2obas  18030  setc2ohom  18031  cat1  18033  0pos  18256  join0  18338  meet0  18339  mgm0b  18594  gsum0  18621  sgrp0b  18665  efmnd0nmnd  18827  pwmnd  18874  mulgfval  19011  ga0  19239  psgn0fv0  19452  pmtrsn  19460  oppglsm  19583  efgi0  19661  vrgpf  19709  vrgpinv  19710  frgpuptinv  19712  frgpup2  19717  0frgp  19720  frgpnabllem1  19814  frgpnabllem2  19815  dprd0  19974  dmdprdpr  19992  dprdpr  19993  00lsp  20944  cnfldfun  21335  cnfldfunOLD  21348  frgpcyg  21540  frlmiscvec  21816  fvcoe1  22160  coe1f2  22162  coe1sfi  22166  coe1add  22218  coe1mul2lem1  22221  coe1mul2lem2  22222  coe1mul2  22223  ply1coe  22254  evls1rhmlem  22277  evl1sca  22290  evl1var  22292  pf1mpf  22308  pf1ind  22311  mat0dimscm  22425  mat0dimcrng  22426  mat0scmat  22494  mavmul0  22508  mavmul0g  22509  mvmumamul1  22510  mdet0pr  22548  mdet0f1o  22549  mdet0fv0  22550  mdetunilem9  22576  d0mat2pmat  22694  chpmat0d  22790  en1top  22940  en2top  22941  sn0topon  22954  indistopon  22957  indistps  22967  indistps2  22968  sn0cld  23046  indiscld  23047  neipeltop  23085  rest0  23125  restsn  23126  cmpfi  23364  refun0  23471  txindislem  23589  hmphindis  23753  xpstopnlem1  23765  xpstopnlem2  23767  ptcmpfi  23769  snfil  23820  fbasfip  23824  fgcl  23834  filconn  23839  fbasrn  23840  cfinfil  23849  csdfil  23850  supfil  23851  ufildr  23887  fin1aufil  23888  rnelfmlem  23908  fclsval  23964  tmdgsum  24051  tsmsfbas  24084  ust0  24176  ustn0  24177  0met  24322  xpsdsval  24337  minveclem3b  25396  tdeglem2  26034  deg1ldg  26065  deg1leb  26068  deg1val  26069  ulm0  26368  nosgnn0  27638  nodense  27672  nolt02o  27675  nogt01o  27676  nulslts  27783  nulsgts  27784  bday1  27822  made0  27871  precsexlem1  28215  precsexlem2  28216  uhgr0  29158  upgr0eop  29199  upgr0eopALT  29201  usgr0  29328  usgr0eop  29331  lfuhgr1v0e  29339  griedg0prc  29349  0grsubgr  29363  cplgr0  29510  0grrusgr  29665  clwwlk0on0  30179  0ewlk  30201  0wlkon  30207  0trlon  30211  0pthon  30214  0pthonv  30216  0conngr  30279  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  wlkl0  30454  disjdifprg  32661  disjun0  32681  of0r  32768  fpwrelmapffslem  32821  f1ocnt  32890  resvsca  33424  1arithidom  33629  vieta  33756  locfinref  34018  zarcmplem  34058  esumnul  34225  esumrnmpt2  34245  prsiga  34308  ldsysgenld  34337  ldgenpisyslem1  34340  oms0  34474  carsggect  34495  eulerpartgbij  34549  eulerpartlemmf  34552  repr0  34788  breprexp  34810  bnj941  34948  bnj97  35041  bnj149  35050  bnj150  35051  bnj944  35113  fineqvac  35291  fineqvnttrclse  35299  wevgblacfn  35322  derang0  35382  indispconn  35447  goeleq12bg  35562  satf0  35585  satf0op  35590  fmla0  35595  fmla0xp  35596  fmlasuc0  35597  fmlafvel  35598  fmlasuc  35599  fmlaomn0  35603  fmla0disjsuc  35611  satfdmfmla  35613  satfv0fvfmla0  35626  sate0  35628  sate0fv0  35630  sategoelfvb  35632  ex-sategoelel  35634  prv0  35643  prv1n  35644  rdgprc  36005  dfrdg3  36007  fullfunfnv  36159  fullfunfv  36160  rank0  36383  ssoninhaus  36661  onint1  36662  bj-0nel1  37198  bj-xpnzex  37204  bj-eltag  37222  bj-0eltag  37223  bj-tagss  37225  bj-pr1val  37249  bj-snex  37280  bj-snfromadj  37289  bj-nuliota  37302  bj-nuliotaALT  37303  bj-rdg0gALT  37316  bj-rest10  37338  bj-rest10b  37339  bj-rest0  37343  rdgssun  37630  finxpreclem1  37641  finxpreclem2  37642  finxp0  37643  finxpreclem5  37647  poimirlem28  37896  heibor1lem  38057  heiborlem6  38064  reheibor  38087  n0elqs  38580  sticksstones11  42523  mzpcompact2lem  43105  wopprc  43384  pw2f1ocnv  43391  pwslnmlem0  43445  pwfi2f1o  43450  2omomeqom  43657  cantnfub  43675  cantnfresb  43678  omcl3g  43688  nadd1suc  43746  naddwordnexlem4  43755  nla0002  43777  nla0003  43778  nla0001  43779  clsk1indlem0  44394  clsk1indlem4  44397  clsk1indlem1  44398  mnupwd  44620  mnuprdlem1  44625  mnuprdlem2  44626  mnuprdlem3  44627  mnurnd  44636  permaxnul  45361  permaxinf2lem  45365  nregmodelf1o  45368  nregmodellem  45369  nregmodel  45370  fnchoice  45386  eliuniincex  45465  limsup0  46049  0cnv  46097  liminf0  46148  0cnf  46232  dvnprodlem3  46303  qndenserrnbl  46650  prsal  46673  intsal  46685  sge00  46731  sge0sn  46734  nnfoctbdjlem  46810  isomenndlem  46885  hoiqssbl  46980  ovnsubadd2lem  47000  iota0def  47395  aiota0def  47453  afv0fv0  47506  0nelsetpreimafv  47747  lincval0  48772  lco0  48784  linds0  48822  0aryfvalel  48991  0aryfvalelfv  48992  1aryenef  49002  2aryenef  49013  mof0  49194  dftpos5  49230  dftpos6  49231  relcic  49401  discsubclem  49419  discsubc  49420  iinfconstbas  49422  nelsubclem  49423  0funcg  49441  0func  49443  0funcALT  49444  oppffn  49480  oppfvalg  49482  fucofvalne  49681  0thinc  49815  setc2othin  49822  setc1ohomfval  49849  setc1ocofval  49850  isinito2lem  49854  prstcthin  49917  setc1onsubc  49958  initocmd  50025  termolmd  50026  bnd2d  50037