Theorem 0ex 5257

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

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

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 5256

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 3446  df-dif 3914  df-nul 4293

This theorem is referenced by:  al0ssb  5258  sseliALT  5259  csbexg  5260  unisn2  5262  class2set  5305  0elpw  5306  0nep0  5308  unidif0  5310  iin0  5312  notzfaus  5313  intv  5314  snexALT  5333  p0ex  5334  dtruALT  5338  zfpair  5371  snex  5386  opex  5419  opthwiener  5469  0sn0ep  5535  opthprc  5695  nrelv  5754  dmsnsnsn  6181  0elon  6375  nsuceq0  6405  snsn0non  6447  iotaex  6472  iotaexOLD  6479  fun0  6565  fvrn0  6870  fvssunirnOLD  6874  fprg  7109  ovima0  7548  onint0  7747  tfinds2  7820  finds  7852  finds2  7854  xpexr  7874  soex  7877  supp0  8121  fvn0elsupp  8136  fvn0elsuppb  8137  brtpos0  8189  reldmtpos  8190  tfrlem16  8338  tz7.44-1  8351  seqomlem1  8395  1n0  8429  nlim1  8430  nlim2  8431  el1o  8436  om0  8458  mapdm0  8792  fsetexb  8814  0map0sn0  8835  ixpexg  8872  0elixp  8879  en0  8966  en0ALT  8967  en0r  8968  ensn1  8969  en1  8972  2dom  8978  map1  8988  enpr2d  8997  xp1en  9004  endisj  9005  pw2eng  9024  0domg  9045  map2xp  9088  limensuci  9094  snnen2o  9161  0sdom1dom  9162  rex2dom  9169  1sdom2dom  9170  1sdomOLD  9172  unxpdom2  9177  sucxpdom  9178  isinf  9183  isinfOLD  9184  ac6sfi  9207  fodomfi  9237  fodomfiOLD  9257  0fsupp  9317  fi0  9347  oiexg  9464  brwdom  9496  brwdom2  9502  inf3lemb  9554  infeq5i  9565  dfom3  9576  cantnfvalf  9594  cantnfval2  9598  cantnfle  9600  cantnflt  9601  cantnff  9603  cantnf0  9604  cantnfp1lem1  9607  cantnfp1lem3  9609  cantnfp1  9610  cantnflem1a  9614  cantnflem1d  9617  cantnflem1  9618  cantnf  9622  cnfcomlem  9628  cnfcom  9629  cnfcom2lem  9630  cnfcom3  9633  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  dmttrcl  9650  ttrclselem2  9655  tc0  9676  r10  9697  scottex  9814  djulcl  9839  djulf1o  9841  djuss  9849  djuun  9855  1stinl  9856  2ndinl  9857  infxpenlem  9942  fseqenlem1  9953  undjudom  10097  endjudisj  10098  djuen  10099  dju1dif  10102  dju1p1e2  10103  dju0en  10105  djucomen  10107  djuassen  10108  xpdjuen  10109  mapdjuen  10110  djuxpdom  10115  djuinf  10118  infdju1  10119  djulepw  10122  pwsdompw  10132  pwdjudom  10144  ackbij1lem14  10161  ackbij2lem2  10168  ackbij2lem3  10169  cf0  10180  cfeq0  10185  cfsuc  10186  cflim2  10192  isfin5  10228  isfin4p1  10244  fin1a2lem11  10339  fin1a2lem12  10340  fin1a2lem13  10341  axcc2lem  10365  ac6num  10408  zornn0g  10434  ttukeylem3  10440  brdom3  10457  iundom2g  10469  cardeq0  10481  pwcfsdom  10512  axpowndlem3  10528  canthwe  10580  canthp1lem1  10581  pwxpndom2  10594  pwdjundom  10596  gchxpidm  10598  intwun  10664  0tsk  10684  grothomex  10758  indpi  10836  fzennn  13909  hash0  14308  hashen1  14311  hashmap  14376  hashbc  14394  hashf1  14398  hashge3el3dif  14428  ccat1st1st  14569  swrdval  14584  swrd00  14585  swrd0  14599  cshfn  14731  cshnz  14733  0csh0  14734  incexclem  15778  incexc  15779  rexpen  16172  sadcf  16399  sadc0  16400  sadcp1  16401  smupf  16424  smup0  16425  smupp1  16426  0ram  16967  ram0  16969  cshws0  17048  str0  17135  ress0  17189  0rest  17368  fnpr2ob  17497  xpsfrnel  17501  xpsle  17518  ismred2  17540  acsfn  17596  0cat  17626  ciclcl  17740  cicrcl  17741  cicer  17744  setcepi  18026  setc2obas  18032  setc2ohom  18033  cat1  18035  0pos  18258  join0  18340  meet0  18341  mgm0b  18560  gsum0  18587  sgrp0b  18631  efmnd0nmnd  18793  pwmnd  18840  mulgfval  18977  ga0  19206  psgn0fv0  19417  pmtrsn  19425  oppglsm  19548  efgi0  19626  vrgpf  19674  vrgpinv  19675  frgpuptinv  19677  frgpup2  19682  0frgp  19685  frgpnabllem1  19779  frgpnabllem2  19780  dprd0  19939  dmdprdpr  19957  dprdpr  19958  00lsp  20863  cnfldfun  21254  cnfldfunOLD  21267  frgpcyg  21459  frlmiscvec  21734  fvcoe1  22068  coe1f2  22070  coe1sfi  22074  coe1add  22126  coe1mul2lem1  22129  coe1mul2lem2  22130  coe1mul2  22131  ply1coe  22161  evls1rhmlem  22184  evl1sca  22197  evl1var  22199  pf1mpf  22215  pf1ind  22218  mat0dimscm  22332  mat0dimcrng  22333  mat0scmat  22401  mavmul0  22415  mavmul0g  22416  mvmumamul1  22417  mdet0pr  22455  mdet0f1o  22456  mdet0fv0  22457  mdetunilem9  22483  d0mat2pmat  22601  chpmat0d  22697  en1top  22847  en2top  22848  sn0topon  22861  indistopon  22864  indistps  22874  indistps2  22875  sn0cld  22953  indiscld  22954  neipeltop  22992  rest0  23032  restsn  23033  cmpfi  23271  refun0  23378  txindislem  23496  hmphindis  23660  xpstopnlem1  23672  xpstopnlem2  23674  ptcmpfi  23676  snfil  23727  fbasfip  23731  fgcl  23741  filconn  23746  fbasrn  23747  cfinfil  23756  csdfil  23757  supfil  23758  ufildr  23794  fin1aufil  23795  rnelfmlem  23815  fclsval  23871  tmdgsum  23958  tsmsfbas  23991  ust0  24083  ustn0  24084  0met  24230  xpsdsval  24245  minveclem3b  25304  tdeglem2  25942  deg1ldg  25973  deg1leb  25976  deg1val  25977  ulm0  26276  nosgnn0  27546  nodense  27580  nolt02o  27583  nogt01o  27584  nulsslt  27685  nulssgt  27686  bday1s  27719  made0  27761  precsexlem1  28085  precsexlem2  28086  uhgr0  28976  upgr0eop  29017  upgr0eopALT  29019  usgr0  29146  usgr0eop  29149  lfuhgr1v0e  29157  griedg0prc  29167  0grsubgr  29181  cplgr0  29328  0grrusgr  29483  clwwlk0on0  29994  0ewlk  30016  0wlkon  30022  0trlon  30026  0pthon  30029  0pthonv  30031  0conngr  30094  konigsberglem1  30154  konigsberglem2  30155  konigsberglem3  30156  wlkl0  30269  disjdifprg  32477  disjun0  32497  of0r  32575  fpwrelmapffslem  32628  f1ocnt  32698  resvsca  33277  1arithidom  33481  locfinref  33804  zarcmplem  33844  esumnul  34011  esumrnmpt2  34031  prsiga  34094  ldsysgenld  34123  ldgenpisyslem1  34126  oms0  34261  carsggect  34282  eulerpartgbij  34336  eulerpartlemmf  34339  repr0  34575  breprexp  34597  bnj941  34735  bnj97  34829  bnj149  34838  bnj150  34839  bnj944  34901  fineqvac  35060  wevgblacfn  35069  derang0  35129  indispconn  35194  goeleq12bg  35309  satf0  35332  satf0op  35337  fmla0  35342  fmla0xp  35343  fmlasuc0  35344  fmlafvel  35345  fmlasuc  35346  fmlaomn0  35350  fmla0disjsuc  35358  satfdmfmla  35360  satfv0fvfmla0  35373  sate0  35375  sate0fv0  35377  sategoelfvb  35379  ex-sategoelel  35381  prv0  35390  prv1n  35391  rdgprc  35755  dfrdg3  35757  fullfunfnv  35907  fullfunfv  35908  rank0  36131  ssoninhaus  36409  onint1  36410  bj-0nel1  36914  bj-xpnzex  36920  bj-eltag  36938  bj-0eltag  36939  bj-tagss  36941  bj-pr1val  36965  bj-snex  36996  bj-snfromadj  37005  bj-nuliota  37018  bj-nuliotaALT  37019  bj-rdg0gALT  37032  bj-rest10  37049  bj-rest10b  37050  bj-rest0  37054  rdgssun  37339  finxpreclem1  37350  finxpreclem2  37351  finxp0  37352  finxpreclem5  37356  poimirlem28  37615  heibor1lem  37776  heiborlem6  37783  reheibor  37806  n0elqs  38287  sticksstones11  42117  mzpcompact2lem  42712  wopprc  42992  pw2f1ocnv  42999  pwslnmlem0  43053  pwfi2f1o  43058  2omomeqom  43265  cantnfub  43283  cantnfresb  43286  omcl3g  43296  nadd1suc  43354  naddwordnexlem4  43363  nla0002  43386  nla0003  43387  nla0001  43388  clsk1indlem0  44003  clsk1indlem4  44006  clsk1indlem1  44007  mnupwd  44229  mnuprdlem1  44234  mnuprdlem2  44235  mnuprdlem3  44236  mnurnd  44245  permaxnul  44971  permaxinf2lem  44975  nregmodelf1o  44978  nregmodellem  44979  nregmodel  44980  fnchoice  44996  eliuniincex  45076  limsup0  45665  0cnv  45713  liminf0  45764  0cnf  45848  dvnprodlem3  45919  qndenserrnbl  46266  prsal  46289  intsal  46301  sge00  46347  sge0sn  46350  nnfoctbdjlem  46426  isomenndlem  46501  hoiqssbl  46596  ovnsubadd2lem  46616  upwordnul  46851  iota0def  47012  aiota0def  47070  afv0fv0  47123  0nelsetpreimafv  47364  lincval0  48377  lco0  48389  linds0  48427  0aryfvalel  48596  0aryfvalelfv  48597  1aryenef  48607  2aryenef  48618  mof0  48799  dftpos5  48835  dftpos6  48836  relcic  49007  discsubclem  49025  discsubc  49026  iinfconstbas  49028  nelsubclem  49029  0funcg  49047  0func  49049  0funcALT  49050  oppffn  49086  oppfvalg  49088  fucofvalne  49287  0thinc  49421  setc2othin  49428  setc1ohomfval  49455  setc1ocofval  49456  isinito2lem  49460  prstcthin  49523  setc1onsubc  49564  initocmd  49631  termolmd  49632  bnd2d  49643