Theorem 0ex 5226

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 5225. (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 5225	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4274	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1851	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3438	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  Vcvv 3422  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-nul 4254

This theorem is referenced by:  al0ssb  5227  sseliALT  5228  csbexg  5229  unisn2  5231  class2set  5271  0elpw  5273  0nep0  5275  unidif0  5277  iin0  5279  notzfaus  5280  intv  5281  snexALT  5301  p0ex  5302  dtruALT  5306  zfpair  5339  snex  5349  dtruALT2  5353  opex  5373  opthwiener  5422  0sn0ep  5490  opthprc  5642  nrelv  5699  dmsnsnsn  6112  0elon  6304  nsuceq0  6331  snsn0non  6370  iotaex  6398  fun0  6483  fvrn0  6784  fvssunirn  6785  fprg  7009  ovima0  7429  onint0  7618  tfinds2  7685  finds  7719  finds2  7721  xpexr  7739  soex  7742  supp0  7953  fvn0elsupp  7967  fvn0elsuppb  7968  brtpos0  8020  reldmtpos  8021  tfrlem16  8195  tz7.44-1  8208  seqomlem1  8251  1n0  8286  el1o  8291  om0  8309  mapdm0  8588  fsetexb  8610  0map0sn0  8631  ixpexg  8668  0elixp  8675  en0  8758  en0OLD  8759  en0ALT  8760  ensn1  8761  ensn1OLD  8762  en1  8765  en1OLD  8766  2dom  8774  map1  8784  xp1en  8798  endisj  8799  pw2eng  8818  map2xp  8883  limensuci  8889  1sdom  8955  unxpdom2  8960  sucxpdom  8961  isinf  8965  ac6sfi  8988  fodomfi  9022  0fsupp  9080  fi0  9109  oiexg  9224  brwdom  9256  brwdom2  9262  inf3lemb  9313  infeq5i  9324  dfom3  9335  cantnfvalf  9353  cantnfval2  9357  cantnfle  9359  cantnflt  9360  cantnff  9362  cantnf0  9363  cantnfp1lem1  9366  cantnfp1lem3  9368  cantnfp1  9369  cantnflem1a  9373  cantnflem1d  9376  cantnflem1  9377  cantnf  9381  cnfcomlem  9387  cnfcom  9388  cnfcom2lem  9389  cnfcom3  9392  trpredpred  9406  trpred0  9410  tc0  9436  r10  9457  scottex  9574  djulcl  9599  djulf1o  9601  djuss  9609  djuun  9615  1stinl  9616  2ndinl  9617  infxpenlem  9700  fseqenlem1  9711  undjudom  9854  endjudisj  9855  djuen  9856  dju1dif  9859  dju1p1e2  9860  dju0en  9862  djucomen  9864  djuassen  9865  xpdjuen  9866  mapdjuen  9867  djuxpdom  9872  djuinf  9875  infdju1  9876  djulepw  9879  pwsdompw  9891  pwdjudom  9903  ackbij1lem14  9920  ackbij2lem2  9927  ackbij2lem3  9928  cf0  9938  cfeq0  9943  cfsuc  9944  cflim2  9950  isfin5  9986  isfin4p1  10002  fin1a2lem11  10097  fin1a2lem12  10098  fin1a2lem13  10099  axcc2lem  10123  ac6num  10166  zornn0g  10192  ttukeylem3  10198  brdom3  10215  iundom2g  10227  cardeq0  10239  pwcfsdom  10270  axpowndlem3  10286  canthwe  10338  canthp1lem1  10339  pwxpndom2  10352  pwdjundom  10354  gchxpidm  10356  intwun  10422  0tsk  10442  grothomex  10516  indpi  10594  fzennn  13616  hash0  14010  hashen1  14013  hashmap  14078  hashbc  14093  hashf1  14099  hashge3el3dif  14128  ccat1st1st  14263  swrdval  14284  swrd00  14285  swrd0  14299  cshfn  14431  cshnz  14433  0csh0  14434  incexclem  15476  incexc  15477  rexpen  15865  sadcf  16088  sadc0  16089  sadcp1  16090  smupf  16113  smup0  16114  smupp1  16115  0ram  16649  ram0  16651  cshws0  16731  str0  16818  ressbasOLD  16874  ress0  16879  0rest  17057  fnpr2ob  17186  xpsfrnel  17190  xpsle  17207  ismred2  17229  acsfn  17285  0cat  17315  ciclcl  17431  cicrcl  17432  cicer  17435  setcepi  17719  setc2obas  17725  setc2ohom  17726  cat1  17728  0pos  17954  0posOLD  17955  join0  18038  meet0  18039  mgm0b  18256  gsum0  18283  sgrp0b  18298  efmnd0nmnd  18444  pwmnd  18491  mulgfval  18617  ga0  18819  psgn0fv0  19034  pmtrsn  19042  oppglsm  19162  efgi0  19241  vrgpf  19289  vrgpinv  19290  frgpuptinv  19292  frgpup2  19297  0frgp  19300  frgpnabllem1  19389  frgpnabllem2  19390  dprd0  19549  dmdprdpr  19567  dprdpr  19568  00lsp  20158  cnfldfunALT  20523  frgpcyg  20693  frlmiscvec  20966  fvcoe1  21288  coe1f2  21290  coe1sfi  21294  coe1add  21345  coe1mul2lem1  21348  coe1mul2lem2  21349  coe1mul2  21350  ply1coe  21377  evls1rhmlem  21397  evl1sca  21410  evl1var  21412  pf1mpf  21428  pf1ind  21431  mat0dimscm  21526  mat0dimcrng  21527  mat0scmat  21595  mavmul0  21609  mavmul0g  21610  mvmumamul1  21611  mdet0pr  21649  mdet0f1o  21650  mdet0fv0  21651  mdetunilem9  21677  d0mat2pmat  21795  chpmat0d  21891  en1top  22042  en2top  22043  sn0topon  22056  indistopon  22059  indistps  22069  indistps2  22070  sn0cld  22149  indiscld  22150  neipeltop  22188  rest0  22228  restsn  22229  cmpfi  22467  refun0  22574  txindislem  22692  hmphindis  22856  xpstopnlem1  22868  xpstopnlem2  22870  ptcmpfi  22872  snfil  22923  fbasfip  22927  fgcl  22937  filconn  22942  fbasrn  22943  cfinfil  22952  csdfil  22953  supfil  22954  ufildr  22990  fin1aufil  22991  rnelfmlem  23011  fclsval  23067  tmdgsum  23154  tsmsfbas  23187  ust0  23279  ustn0  23280  0met  23427  xpsdsval  23442  minveclem3b  24497  tdeglem2  25131  deg1ldg  25162  deg1leb  25165  deg1val  25166  ulm0  25455  uhgr0  27346  upgr0eop  27387  upgr0eopALT  27389  usgr0  27513  usgr0eop  27516  lfuhgr1v0e  27524  griedg0prc  27534  0grsubgr  27548  cplgr0  27695  0grrusgr  27849  clwwlk0on0  28357  0ewlk  28379  0wlkon  28385  0trlon  28389  0pthon  28392  0pthonv  28394  0conngr  28457  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519  wlkl0  28632  disjdifprg  30815  disjun0  30835  fpwrelmapffslem  30969  f1ocnt  31025  resvsca  31431  locfinref  31693  zarcmplem  31733  esumnul  31916  esumrnmpt2  31936  prsiga  31999  ldsysgenld  32028  ldgenpisyslem1  32031  oms0  32164  carsggect  32185  eulerpartgbij  32239  eulerpartlemmf  32242  repr0  32491  breprexp  32513  bnj941  32652  bnj97  32746  bnj149  32755  bnj150  32756  bnj944  32818  fineqvac  32966  derang0  33031  indispconn  33096  goeleq12bg  33211  satf0  33234  satf0op  33239  fmla0  33244  fmla0xp  33245  fmlasuc0  33246  fmlafvel  33247  fmlasuc  33248  fmlaomn0  33252  fmla0disjsuc  33260  satfdmfmla  33262  satfv0fvfmla0  33275  sate0  33277  sate0fv0  33279  sategoelfvb  33281  ex-sategoelel  33283  prv0  33292  prv1n  33293  rdgprc  33676  dfrdg3  33678  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  dmttrcl  33707  ttrclselem2  33712  nosgnn0  33788  nodense  33822  nolt02o  33825  nogt01o  33826  nulsslt  33918  nulssgt  33919  bday1s  33952  made0  33984  fullfunfnv  34175  fullfunfv  34176  rank0  34399  ssoninhaus  34564  onint1  34565  bj-0nel1  35070  bj-xpnzex  35076  bj-eltag  35094  bj-0eltag  35095  bj-tagss  35097  bj-pr1val  35121  bj-nuliota  35155  bj-nuliotaALT  35156  bj-rdg0gALT  35169  bj-rest10  35186  bj-rest10b  35187  bj-rest0  35191  rdgssun  35476  finxpreclem1  35487  finxpreclem2  35488  finxp0  35489  finxpreclem5  35493  poimirlem28  35732  heibor1lem  35894  heiborlem6  35901  reheibor  35924  n0elqs  36388  sticksstones11  40040  sn-iotaex  40123  mzpcompact2lem  40489  wopprc  40768  pw2f1ocnv  40775  pwslnmlem0  40832  pwfi2f1o  40837  clsk1indlem0  41540  clsk1indlem4  41543  clsk1indlem1  41544  mnupwd  41774  mnuprdlem1  41779  mnuprdlem2  41780  mnuprdlem3  41781  mnurnd  41790  fnchoice  42461  eliuniincex  42548  limsup0  43125  0cnv  43173  liminf0  43224  0cnf  43308  dvnprodlem3  43379  qndenserrnbl  43726  prsal  43749  intsal  43759  sge00  43804  sge0sn  43807  nnfoctbdjlem  43883  isomenndlem  43958  hoiqssbl  44053  ovnsubadd2lem  44073  iota0def  44419  aiota0def  44475  afv0fv0  44528  0nelsetpreimafv  44730  lincval0  45644  lco0  45656  linds0  45694  0aryfvalel  45868  0aryfvalelfv  45869  1aryenef  45879  2aryenef  45890  mof0  46053  0thinc  46220  setc2othin  46225  prstcthin  46243  bnd2d  46273