Theorem 0ex 5307

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

Syntax hints:  ¬ wn 3  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3480  ∅c0 4333

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-nul 4334

This theorem is referenced by:  al0ssb  5308  sseliALT  5309  csbexg  5310  unisn2  5312  class2set  5355  0elpw  5356  0nep0  5358  unidif0  5360  iin0  5362  notzfaus  5363  intv  5364  snexALT  5383  p0ex  5384  dtruALT  5388  zfpair  5421  snex  5436  opex  5469  opthwiener  5519  0sn0ep  5588  opthprc  5749  nrelv  5810  dmsnsnsn  6240  0elon  6438  nsuceq0  6467  snsn0non  6509  iotaex  6534  iotaexOLD  6541  fun0  6631  fvrn0  6936  fvssunirnOLD  6940  fprg  7175  ovima0  7612  onint0  7811  tfinds2  7885  finds  7918  finds2  7920  xpexr  7940  soex  7943  supp0  8190  fvn0elsupp  8205  fvn0elsuppb  8206  brtpos0  8258  reldmtpos  8259  tfrlem16  8433  tz7.44-1  8446  seqomlem1  8490  1n0  8526  nlim1  8527  nlim2  8528  el1o  8533  om0  8555  mapdm0  8882  fsetexb  8904  0map0sn0  8925  ixpexg  8962  0elixp  8969  en0  9058  en0ALT  9059  en0r  9060  ensn1  9061  en1  9064  2dom  9070  map1  9080  enpr2d  9089  xp1en  9097  endisj  9098  pw2eng  9118  0domg  9140  map2xp  9187  limensuci  9193  snnen2o  9273  0sdom1dom  9274  rex2dom  9282  1sdom2dom  9283  1sdomOLD  9285  unxpdom2  9290  sucxpdom  9291  isinf  9296  isinfOLD  9297  ac6sfi  9320  fodomfi  9350  fodomfiOLD  9370  0fsupp  9430  fi0  9460  oiexg  9575  brwdom  9607  brwdom2  9613  inf3lemb  9665  infeq5i  9676  dfom3  9687  cantnfvalf  9705  cantnfval2  9709  cantnfle  9711  cantnflt  9712  cantnff  9714  cantnf0  9715  cantnfp1lem1  9718  cantnfp1lem3  9720  cantnfp1  9721  cantnflem1a  9725  cantnflem1d  9728  cantnflem1  9729  cantnf  9733  cnfcomlem  9739  cnfcom  9740  cnfcom2lem  9741  cnfcom3  9744  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  dmttrcl  9761  ttrclselem2  9766  tc0  9787  r10  9808  scottex  9925  djulcl  9950  djulf1o  9952  djuss  9960  djuun  9966  1stinl  9967  2ndinl  9968  infxpenlem  10053  fseqenlem1  10064  undjudom  10208  endjudisj  10209  djuen  10210  dju1dif  10213  dju1p1e2  10214  dju0en  10216  djucomen  10218  djuassen  10219  xpdjuen  10220  mapdjuen  10221  djuxpdom  10226  djuinf  10229  infdju1  10230  djulepw  10233  pwsdompw  10243  pwdjudom  10255  ackbij1lem14  10272  ackbij2lem2  10279  ackbij2lem3  10280  cf0  10291  cfeq0  10296  cfsuc  10297  cflim2  10303  isfin5  10339  isfin4p1  10355  fin1a2lem11  10450  fin1a2lem12  10451  fin1a2lem13  10452  axcc2lem  10476  ac6num  10519  zornn0g  10545  ttukeylem3  10551  brdom3  10568  iundom2g  10580  cardeq0  10592  pwcfsdom  10623  axpowndlem3  10639  canthwe  10691  canthp1lem1  10692  pwxpndom2  10705  pwdjundom  10707  gchxpidm  10709  intwun  10775  0tsk  10795  grothomex  10869  indpi  10947  fzennn  14009  hash0  14406  hashen1  14409  hashmap  14474  hashbc  14492  hashf1  14496  hashge3el3dif  14526  ccat1st1st  14666  swrdval  14681  swrd00  14682  swrd0  14696  cshfn  14828  cshnz  14830  0csh0  14831  incexclem  15872  incexc  15873  rexpen  16264  sadcf  16490  sadc0  16491  sadcp1  16492  smupf  16515  smup0  16516  smupp1  16517  0ram  17058  ram0  17060  cshws0  17139  str0  17226  ressbasOLD  17281  ress0  17289  0rest  17474  fnpr2ob  17603  xpsfrnel  17607  xpsle  17624  ismred2  17646  acsfn  17702  0cat  17732  ciclcl  17846  cicrcl  17847  cicer  17850  setcepi  18133  setc2obas  18139  setc2ohom  18140  cat1  18142  0pos  18367  join0  18450  meet0  18451  mgm0b  18670  gsum0  18697  sgrp0b  18741  efmnd0nmnd  18903  pwmnd  18950  mulgfval  19087  ga0  19316  psgn0fv0  19529  pmtrsn  19537  oppglsm  19660  efgi0  19738  vrgpf  19786  vrgpinv  19787  frgpuptinv  19789  frgpup2  19794  0frgp  19797  frgpnabllem1  19891  frgpnabllem2  19892  dprd0  20051  dmdprdpr  20069  dprdpr  20070  00lsp  20979  cnfldfun  21378  cnfldfunOLD  21391  frgpcyg  21592  frlmiscvec  21869  fvcoe1  22209  coe1f2  22211  coe1sfi  22215  coe1add  22267  coe1mul2lem1  22270  coe1mul2lem2  22271  coe1mul2  22272  ply1coe  22302  evls1rhmlem  22325  evl1sca  22338  evl1var  22340  pf1mpf  22356  pf1ind  22359  mat0dimscm  22475  mat0dimcrng  22476  mat0scmat  22544  mavmul0  22558  mavmul0g  22559  mvmumamul1  22560  mdet0pr  22598  mdet0f1o  22599  mdet0fv0  22600  mdetunilem9  22626  d0mat2pmat  22744  chpmat0d  22840  en1top  22991  en2top  22992  sn0topon  23005  indistopon  23008  indistps  23018  indistps2  23019  sn0cld  23098  indiscld  23099  neipeltop  23137  rest0  23177  restsn  23178  cmpfi  23416  refun0  23523  txindislem  23641  hmphindis  23805  xpstopnlem1  23817  xpstopnlem2  23819  ptcmpfi  23821  snfil  23872  fbasfip  23876  fgcl  23886  filconn  23891  fbasrn  23892  cfinfil  23901  csdfil  23902  supfil  23903  ufildr  23939  fin1aufil  23940  rnelfmlem  23960  fclsval  24016  tmdgsum  24103  tsmsfbas  24136  ust0  24228  ustn0  24229  0met  24376  xpsdsval  24391  minveclem3b  25462  tdeglem2  26100  deg1ldg  26131  deg1leb  26134  deg1val  26135  ulm0  26434  nosgnn0  27703  nodense  27737  nolt02o  27740  nogt01o  27741  nulsslt  27842  nulssgt  27843  bday1s  27876  made0  27912  precsexlem1  28231  precsexlem2  28232  uhgr0  29090  upgr0eop  29131  upgr0eopALT  29133  usgr0  29260  usgr0eop  29263  lfuhgr1v0e  29271  griedg0prc  29281  0grsubgr  29295  cplgr0  29442  0grrusgr  29597  clwwlk0on0  30111  0ewlk  30133  0wlkon  30139  0trlon  30143  0pthon  30146  0pthonv  30148  0conngr  30211  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  wlkl0  30386  disjdifprg  32588  disjun0  32608  of0r  32688  fpwrelmapffslem  32743  f1ocnt  32804  resvsca  33356  1arithidom  33565  locfinref  33840  zarcmplem  33880  esumnul  34049  esumrnmpt2  34069  prsiga  34132  ldsysgenld  34161  ldgenpisyslem1  34164  oms0  34299  carsggect  34320  eulerpartgbij  34374  eulerpartlemmf  34377  repr0  34626  breprexp  34648  bnj941  34786  bnj97  34880  bnj149  34889  bnj150  34890  bnj944  34952  fineqvac  35111  wevgblacfn  35114  derang0  35174  indispconn  35239  goeleq12bg  35354  satf0  35377  satf0op  35382  fmla0  35387  fmla0xp  35388  fmlasuc0  35389  fmlafvel  35390  fmlasuc  35391  fmlaomn0  35395  fmla0disjsuc  35403  satfdmfmla  35405  satfv0fvfmla0  35418  sate0  35420  sate0fv0  35422  sategoelfvb  35424  ex-sategoelel  35426  prv0  35435  prv1n  35436  rdgprc  35795  dfrdg3  35797  fullfunfnv  35947  fullfunfv  35948  rank0  36171  ssoninhaus  36449  onint1  36450  bj-0nel1  36954  bj-xpnzex  36960  bj-eltag  36978  bj-0eltag  36979  bj-tagss  36981  bj-pr1val  37005  bj-snex  37036  bj-snfromadj  37045  bj-nuliota  37058  bj-nuliotaALT  37059  bj-rdg0gALT  37072  bj-rest10  37089  bj-rest10b  37090  bj-rest0  37094  rdgssun  37379  finxpreclem1  37390  finxpreclem2  37391  finxp0  37392  finxpreclem5  37396  poimirlem28  37655  heibor1lem  37816  heiborlem6  37823  reheibor  37846  n0elqs  38327  sticksstones11  42157  mzpcompact2lem  42762  wopprc  43042  pw2f1ocnv  43049  pwslnmlem0  43103  pwfi2f1o  43108  2omomeqom  43316  cantnfub  43334  cantnfresb  43337  omcl3g  43347  nadd1suc  43405  naddwordnexlem4  43414  nla0002  43437  nla0003  43438  nla0001  43439  clsk1indlem0  44054  clsk1indlem4  44057  clsk1indlem1  44058  mnupwd  44286  mnuprdlem1  44291  mnuprdlem2  44292  mnuprdlem3  44293  mnurnd  44302  fnchoice  45034  eliuniincex  45114  limsup0  45709  0cnv  45757  liminf0  45808  0cnf  45892  dvnprodlem3  45963  qndenserrnbl  46310  prsal  46333  intsal  46345  sge00  46391  sge0sn  46394  nnfoctbdjlem  46470  isomenndlem  46545  hoiqssbl  46640  ovnsubadd2lem  46660  upwordnul  46895  iota0def  47050  aiota0def  47108  afv0fv0  47161  0nelsetpreimafv  47377  lincval0  48332  lco0  48344  linds0  48382  0aryfvalel  48555  0aryfvalelfv  48556  1aryenef  48566  2aryenef  48577  mof0  48747  dftpos5  48774  dftpos6  48775  0funcg  48918  0func  48920  0funcALT  48921  fucofvalne  49020  0thinc  49108  setc2othin  49113  prstcthin  49165  bnd2d  49200