Theorem 0ex 5312

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

Syntax hints:  ¬ wn 3  ∀wal 1534   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-nul 4339

This theorem is referenced by:  al0ssb  5313  sseliALT  5314  csbexg  5315  unisn2  5317  class2set  5360  0elpw  5361  0nep0  5363  unidif0  5365  iin0  5367  notzfaus  5368  intv  5369  snexALT  5388  p0ex  5389  dtruALT  5393  zfpair  5426  snex  5441  opex  5474  opthwiener  5523  0sn0ep  5592  opthprc  5752  nrelv  5812  dmsnsnsn  6241  0elon  6439  nsuceq0  6468  snsn0non  6510  iotaex  6535  iotaexOLD  6542  fun0  6632  fvrn0  6936  fvssunirnOLD  6940  fprg  7174  ovima0  7611  onint0  7810  tfinds2  7884  finds  7918  finds2  7920  xpexr  7940  soex  7943  supp0  8188  fvn0elsupp  8203  fvn0elsuppb  8204  brtpos0  8256  reldmtpos  8257  tfrlem16  8431  tz7.44-1  8444  seqomlem1  8488  1n0  8524  nlim1  8525  nlim2  8526  el1o  8531  om0  8553  mapdm0  8880  fsetexb  8902  0map0sn0  8923  ixpexg  8960  0elixp  8967  en0  9056  en0ALT  9057  en0r  9058  ensn1  9059  en1  9062  2dom  9068  map1  9078  enpr2d  9087  xp1en  9095  endisj  9096  pw2eng  9116  0domg  9138  map2xp  9185  limensuci  9191  snnen2o  9270  0sdom1dom  9271  rex2dom  9279  1sdom2dom  9280  1sdomOLD  9282  unxpdom2  9287  sucxpdom  9288  isinf  9293  isinfOLD  9294  ac6sfi  9317  fodomfi  9347  fodomfiOLD  9367  0fsupp  9427  fi0  9457  oiexg  9572  brwdom  9604  brwdom2  9610  inf3lemb  9662  infeq5i  9673  dfom3  9684  cantnfvalf  9702  cantnfval2  9706  cantnfle  9708  cantnflt  9709  cantnff  9711  cantnf0  9712  cantnfp1lem1  9715  cantnfp1lem3  9717  cantnfp1  9718  cantnflem1a  9722  cantnflem1d  9725  cantnflem1  9726  cantnf  9730  cnfcomlem  9736  cnfcom  9737  cnfcom2lem  9738  cnfcom3  9741  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  dmttrcl  9758  ttrclselem2  9763  tc0  9784  r10  9805  scottex  9922  djulcl  9947  djulf1o  9949  djuss  9957  djuun  9963  1stinl  9964  2ndinl  9965  infxpenlem  10050  fseqenlem1  10061  undjudom  10205  endjudisj  10206  djuen  10207  dju1dif  10210  dju1p1e2  10211  dju0en  10213  djucomen  10215  djuassen  10216  xpdjuen  10217  mapdjuen  10218  djuxpdom  10223  djuinf  10226  infdju1  10227  djulepw  10230  pwsdompw  10240  pwdjudom  10252  ackbij1lem14  10269  ackbij2lem2  10276  ackbij2lem3  10277  cf0  10288  cfeq0  10293  cfsuc  10294  cflim2  10300  isfin5  10336  isfin4p1  10352  fin1a2lem11  10447  fin1a2lem12  10448  fin1a2lem13  10449  axcc2lem  10473  ac6num  10516  zornn0g  10542  ttukeylem3  10548  brdom3  10565  iundom2g  10577  cardeq0  10589  pwcfsdom  10620  axpowndlem3  10636  canthwe  10688  canthp1lem1  10689  pwxpndom2  10702  pwdjundom  10704  gchxpidm  10706  intwun  10772  0tsk  10792  grothomex  10866  indpi  10944  fzennn  14005  hash0  14402  hashen1  14405  hashmap  14470  hashbc  14488  hashf1  14492  hashge3el3dif  14522  ccat1st1st  14662  swrdval  14677  swrd00  14678  swrd0  14692  cshfn  14824  cshnz  14826  0csh0  14827  incexclem  15868  incexc  15869  rexpen  16260  sadcf  16486  sadc0  16487  sadcp1  16488  smupf  16511  smup0  16512  smupp1  16513  0ram  17053  ram0  17055  cshws0  17135  str0  17222  ressbasOLD  17280  ress0  17288  0rest  17475  fnpr2ob  17604  xpsfrnel  17608  xpsle  17625  ismred2  17647  acsfn  17703  0cat  17733  ciclcl  17849  cicrcl  17850  cicer  17853  setcepi  18141  setc2obas  18147  setc2ohom  18148  cat1  18150  0pos  18378  0posOLD  18379  join0  18462  meet0  18463  mgm0b  18682  gsum0  18709  sgrp0b  18753  efmnd0nmnd  18915  pwmnd  18962  mulgfval  19099  ga0  19328  psgn0fv0  19543  pmtrsn  19551  oppglsm  19674  efgi0  19752  vrgpf  19800  vrgpinv  19801  frgpuptinv  19803  frgpup2  19808  0frgp  19811  frgpnabllem1  19905  frgpnabllem2  19906  dprd0  20065  dmdprdpr  20083  dprdpr  20084  00lsp  20996  cnfldfun  21395  cnfldfunOLD  21408  frgpcyg  21609  frlmiscvec  21886  fvcoe1  22224  coe1f2  22226  coe1sfi  22230  coe1add  22282  coe1mul2lem1  22285  coe1mul2lem2  22286  coe1mul2  22287  ply1coe  22317  evls1rhmlem  22340  evl1sca  22353  evl1var  22355  pf1mpf  22371  pf1ind  22374  mat0dimscm  22490  mat0dimcrng  22491  mat0scmat  22559  mavmul0  22573  mavmul0g  22574  mvmumamul1  22575  mdet0pr  22613  mdet0f1o  22614  mdet0fv0  22615  mdetunilem9  22641  d0mat2pmat  22759  chpmat0d  22855  en1top  23006  en2top  23007  sn0topon  23020  indistopon  23023  indistps  23033  indistps2  23034  sn0cld  23113  indiscld  23114  neipeltop  23152  rest0  23192  restsn  23193  cmpfi  23431  refun0  23538  txindislem  23656  hmphindis  23820  xpstopnlem1  23832  xpstopnlem2  23834  ptcmpfi  23836  snfil  23887  fbasfip  23891  fgcl  23901  filconn  23906  fbasrn  23907  cfinfil  23916  csdfil  23917  supfil  23918  ufildr  23954  fin1aufil  23955  rnelfmlem  23975  fclsval  24031  tmdgsum  24118  tsmsfbas  24151  ust0  24243  ustn0  24244  0met  24391  xpsdsval  24406  minveclem3b  25475  tdeglem2  26114  deg1ldg  26145  deg1leb  26148  deg1val  26149  ulm0  26448  nosgnn0  27717  nodense  27751  nolt02o  27754  nogt01o  27755  nulsslt  27856  nulssgt  27857  bday1s  27890  made0  27926  precsexlem1  28245  precsexlem2  28246  uhgr0  29104  upgr0eop  29145  upgr0eopALT  29147  usgr0  29274  usgr0eop  29277  lfuhgr1v0e  29285  griedg0prc  29295  0grsubgr  29309  cplgr0  29456  0grrusgr  29611  clwwlk0on0  30120  0ewlk  30142  0wlkon  30148  0trlon  30152  0pthon  30155  0pthonv  30157  0conngr  30220  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  wlkl0  30395  disjdifprg  32594  disjun0  32614  of0r  32694  fpwrelmapffslem  32749  f1ocnt  32809  resvsca  33335  1arithidom  33544  locfinref  33801  zarcmplem  33841  esumnul  34028  esumrnmpt2  34048  prsiga  34111  ldsysgenld  34140  ldgenpisyslem1  34143  oms0  34278  carsggect  34299  eulerpartgbij  34353  eulerpartlemmf  34356  repr0  34604  breprexp  34626  bnj941  34764  bnj97  34858  bnj149  34867  bnj150  34868  bnj944  34930  fineqvac  35089  wevgblacfn  35092  derang0  35153  indispconn  35218  goeleq12bg  35333  satf0  35356  satf0op  35361  fmla0  35366  fmla0xp  35367  fmlasuc0  35368  fmlafvel  35369  fmlasuc  35370  fmlaomn0  35374  fmla0disjsuc  35382  satfdmfmla  35384  satfv0fvfmla0  35397  sate0  35399  sate0fv0  35401  sategoelfvb  35403  ex-sategoelel  35405  prv0  35414  prv1n  35415  rdgprc  35775  dfrdg3  35777  fullfunfnv  35927  fullfunfv  35928  rank0  36151  ssoninhaus  36430  onint1  36431  bj-0nel1  36935  bj-xpnzex  36941  bj-eltag  36959  bj-0eltag  36960  bj-tagss  36962  bj-pr1val  36986  bj-snex  37017  bj-snfromadj  37026  bj-nuliota  37039  bj-nuliotaALT  37040  bj-rdg0gALT  37053  bj-rest10  37070  bj-rest10b  37071  bj-rest0  37075  rdgssun  37360  finxpreclem1  37371  finxpreclem2  37372  finxp0  37373  finxpreclem5  37377  poimirlem28  37634  heibor1lem  37795  heiborlem6  37802  reheibor  37825  n0elqs  38307  sticksstones11  42137  mzpcompact2lem  42738  wopprc  43018  pw2f1ocnv  43025  pwslnmlem0  43079  pwfi2f1o  43084  2omomeqom  43292  cantnfub  43310  cantnfresb  43313  omcl3g  43323  nadd1suc  43381  naddwordnexlem4  43390  nla0002  43413  nla0003  43414  nla0001  43415  clsk1indlem0  44030  clsk1indlem4  44033  clsk1indlem1  44034  mnupwd  44262  mnuprdlem1  44267  mnuprdlem2  44268  mnuprdlem3  44269  mnurnd  44278  fnchoice  44966  eliuniincex  45048  limsup0  45649  0cnv  45697  liminf0  45748  0cnf  45832  dvnprodlem3  45903  qndenserrnbl  46250  prsal  46273  intsal  46285  sge00  46331  sge0sn  46334  nnfoctbdjlem  46410  isomenndlem  46485  hoiqssbl  46580  ovnsubadd2lem  46600  upwordnul  46833  iota0def  46987  aiota0def  47045  afv0fv0  47098  0nelsetpreimafv  47314  lincval0  48260  lco0  48272  linds0  48310  0aryfvalel  48483  0aryfvalelfv  48484  1aryenef  48494  2aryenef  48505  mof0  48667  0thinc  48851  setc2othin  48856  prstcthin  48876  bnd2d  48911