Theorem 0ex 4718

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 4717. (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 4717	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 3888	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1764	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 220	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3183	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  sseliALT  4719  csbexg  4720  unisn2  4722  class2set  4758  0elpw  4760  0nep0  4762  unidif0  4764  iin0  4765  notzfaus  4766  intv  4767  snexALT  4778  p0ex  4779  dtruALT  4826  zfpair  4831  snex  4835  dtruALT2  4838  opex  4859  opthwiener  4901  opthprc  5089  dmsnsnsn  5531  0elon  5695  nsuceq0  5722  snsn0non  5763  iotaex  5785  nfunv  5835  fun0  5868  fvrn0  6126  fvssunirn  6127  fprg  6327  ovima0  6711  onint0  6888  tfinds2  6955  finds  6984  finds2  6986  xpexr  6999  soex  7002  supp0  7187  fvn0elsupp  7198  fvn0elsuppb  7199  brtpos0  7246  reldmtpos  7247  tfrlem16  7376  tz7.44-1  7389  seqomlem1  7432  1n0  7462  el1o  7466  om0  7484  map0e  7781  ixpexg  7818  0elixp  7825  en0  7905  ensn1  7906  en1  7909  2dom  7915  map1  7921  xp1en  7931  endisj  7932  pw2eng  7951  map2xp  8015  limensuci  8021  1sdom  8048  unxpdom2  8053  sucxpdom  8054  isinf  8058  ac6sfi  8089  fodomfi  8124  0fsupp  8180  fi0  8209  oiexg  8323  brwdom  8355  brwdom2  8361  inf3lemb  8405  infeq5i  8416  dfom3  8427  cantnfvalf  8445  cantnfval2  8449  cantnfle  8451  cantnflt  8452  cantnff  8454  cantnf0  8455  cantnfp1lem1  8458  cantnfp1lem2  8459  cantnfp1lem3  8460  cantnfp1  8461  cantnflem1a  8465  cantnflem1d  8468  cantnflem1  8469  cantnflem3  8471  cantnf  8473  cnfcomlem  8479  cnfcom  8480  cnfcom2lem  8481  cnfcom3  8484  tc0  8506  r10  8514  scottex  8631  infxpenlem  8719  fseqenlem1  8730  uncdadom  8876  cdaun  8877  cdaen  8878  cda1dif  8881  pm110.643  8882  cda0en  8884  cdacomen  8886  cdaassen  8887  xpcdaen  8888  mapcdaen  8889  cdaxpdom  8894  cdainf  8897  infcda1  8898  pwsdompw  8909  pwcdadom  8921  ackbij1lem14  8938  ackbij2lem2  8945  ackbij2lem3  8946  cf0  8956  cfeq0  8961  cfsuc  8962  cflim2  8968  isfin5  9004  isfin4-3  9020  fin1a2lem11  9115  fin1a2lem12  9116  fin1a2lem13  9117  axcc2lem  9141  ac6num  9184  zornn0g  9210  ttukeylem3  9216  brdom3  9231  iundom2g  9241  cardeq0  9253  alephadd  9278  pwcfsdom  9284  axpowndlem3  9300  canthwe  9352  canthp1lem1  9353  pwxpndom2  9366  pwcdandom  9368  gchxpidm  9370  intwun  9436  0tsk  9456  grothomex  9530  indpi  9608  fzennn  12629  hash0  13019  hashen1  13021  hashmap  13082  hashbc  13094  hashf1  13098  hashge3el3dif  13122  swrdval  13269  swrd00  13270  swrd0  13286  cshfn  13387  cshnz  13389  0csh0  13390  incexclem  14407  incexc  14408  rexpen  14796  sadcf  15013  sadc0  15014  sadcp1  15015  smupf  15038  smup0  15039  smupp1  15040  0ram  15562  ram0  15564  cshws0  15646  str0  15739  ressbas  15757  ress0  15761  0rest  15913  xpscg  16041  xpscfn  16042  xpsc0  16043  xpsc1  16044  xpsfrnel  16046  xpsfrnel2  16048  xpsle  16064  ismred2  16086  acsfn  16143  0cat  16172  ciclcl  16285  cicrcl  16286  cicer  16289  setcepi  16561  0pos  16777  meet0  16960  join0  16961  mgm0b  17079  gsum0  17101  sgrp0b  17115  ga0  17554  psgn0fv0  17754  pmtrsn  17762  oppglsm  17880  efgi0  17956  vrgpf  18004  vrgpinv  18005  frgpuptinv  18007  frgpup2  18012  0frgp  18015  frgpnabllem1  18099  frgpnabllem2  18100  dprd0  18253  dmdprdpr  18271  dprdpr  18272  00lsp  18802  fvcoe1  19398  coe1f2  19400  coe1sfi  19404  coe1add  19455  coe1mul2lem1  19458  coe1mul2lem2  19459  coe1mul2  19460  ply1coe  19487  evls1rhmlem  19507  evl1sca  19519  evl1var  19521  pf1mpf  19537  pf1ind  19540  frgpcyg  19741  frlmiscvec  20007  mat0dimscm  20094  mat0dimcrng  20095  mat0scmat  20163  mavmul0  20177  mavmul0g  20178  mvmumamul1  20179  mdet0pr  20217  mdet0f1o  20218  mdet0fv0  20219  mdetunilem9  20245  d0mat2pmat  20362  chpmat0d  20458  topgele  20549  en1top  20599  en2top  20600  sn0topon  20612  indistopon  20615  indistps  20625  indistps2  20626  sn0cld  20704  indiscld  20705  neipeltop  20743  rest0  20783  restsn  20784  cmpfi  21021  refun0  21128  txindislem  21246  hmphindis  21410  xpstopnlem1  21422  xpstopnlem2  21424  ptcmpfi  21426  snfil  21478  fbasfip  21482  fgcl  21492  filcon  21497  fbasrn  21498  cfinfil  21507  csdfil  21508  supfil  21509  ufildr  21545  fin1aufil  21546  rnelfmlem  21566  fclsval  21622  tmdgsum  21709  tsmsfbas  21741  ust0  21833  ustn0  21834  0met  21981  xpsdsval  21996  minveclem3b  23007  tdeglem2  23625  deg1ldg  23656  deg1leb  23659  deg1val  23660  ulm0  23949  vtxval0  25714  iedgval0  25715  uhgr0  25739  upgr0eop  25780  upgr0eopALT  25782  uhgra0  25838  uhgra0v  25839  umgra0  25854  usgra0  25899  usgra0v  25900  cusgra0v  25989  cusgra1v  25990  uvtx01vtx  26020  0wlk  26075  0trl  26076  0wlkon  26077  0trlon  26078  0pth  26100  0spth  26101  0pthon  26109  0pthonv  26111  0crct  26154  0cycl  26155  0conngra  26202  0clwlk  26293  vdgr0  26427  0egra0rgra  26463  0vgrargra  26464  frgra0v  26520  2spot0  26591  disjdifprg  28770  disjun0  28790  fpwrelmapffslem  28895  f1ocnt  28946  resvsca  29161  locfinref  29236  esumnul  29437  esumrnmpt2  29457  prsiga  29521  ldsysgenld  29550  ldgenpisyslem1  29553  oms0  29686  carsggect  29707  eulerpartgbij  29761  eulerpartlemmf  29764  bnj941  30097  bnj97  30190  bnj149  30199  bnj150  30200  bnj944  30262  derang0  30405  indispcon  30470  rdgprc  30944  dfrdg3  30946  trpredpred  30972  trpred0  30980  nosgnn0  31055  nodense  31088  fullfunfnv  31223  fullfunfv  31224  rank0  31447  ssoninhaus  31617  onint1  31618  bj-1ex  32131  bj-0nel1  32133  bj-xpnzex  32139  bj-eltag  32158  bj-0eltag  32159  bj-tagss  32161  bj-pr1val  32185  bj-nuliota  32210  bj-nuliotaALT  32211  bj-rest10  32222  bj-rest10b  32223  bj-rest0  32227  finxpreclem1  32402  finxpreclem2  32403  finxp0  32404  finxpreclem5  32408  poimirlem28  32607  heibor1lem  32778  heiborlem6  32785  reheibor  32808  mzpcompact2lem  36332  wopprc  36615  pw2f1ocnv  36622  pwslnmlem0  36679  pwfi2f1o  36684  relintabex  36906  clsk1indlem0  37359  clsk1indlem4  37362  clsk1indlem1  37363  fnchoice  38211  eliuniincex  38323  mapdm0  38378  0cnf  38762  dvnprodlem3  38838  qndenserrnbl  39191  prsal  39214  intsal  39224  sge00  39269  sge0sn  39272  nnfoctbdjlem  39348  isomenndlem  39420  hoiqssbl  39515  ovnsubadd2lem  39535  afv0fv0  39878  usgr0  40469  usgr0eop  40472  lfuhgr1v0e  40480  griedg0prc  40488  0grsubgr  40502  cplgr0  40647  0grrusgr  40779  0ewlk  41282  01wlk  41284  0wlkOn  41288  0Trl  41290  0TrlOn  41292  0pth-av  41293  0spth-av  41294  0pthon-av  41295  0pthonv-av  41297  0Crct  41300  0Cycl  41301  0conngr  41359  eupth0  41382  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424  lincval0  41998  lco0  42010  linds0  42048  bnd2d  42226