Theorem 0ex 4567

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 4566. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Assertion

Ref	Expression
0ex	|- (/) e. _V

Proof of Theorem 0ex

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-nul 4566	. . 3 |- E. x A. y -. y e. x
2		eq0 3786	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1654	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 209	. 2 |- E. x x = (/)
5	4	issetri 3102	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1381   = wceq 1383   E.wex 1599   e. wcel 1804   _Vcvv 3095   (/)c0 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-nul 4566

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-v 3097  df-dif 3464  df-nul 3771

This theorem is referenced by:  sseliALT  4568  csbexg  4569  unisn2  4573  class2set  4604  0elpw  4606  0nep0  4608  unidif0  4610  iin0  4611  notzfaus  4612  intv  4613  snexALT  4623  p0ex  4624  dtruALT  4669  zfpair  4674  snex  4678  dtruALT2  4681  opex  4701  opthwiener  4739  0elon  4921  nsuceq0  4948  snsn0non  4986  opthprc  5037  dmsnsnsn  5476  iotaex  5558  nfunv  5609  fun0  5635  fvrn0  5878  fvssunirn  5879  fprg  6065  ovima0  6439  onint0  6616  tfinds2  6683  finds  6711  finds2  6713  xpexr  6725  soex  6728  supp0  6908  fvn0elsupp  6919  brtpos0  6964  reldmtpos  6965  tfrlem16  7064  tz7.44-1  7074  seqomlem1  7117  1n0  7147  el1o  7151  om0  7169  map0e  7458  ixpexg  7495  0elixp  7502  en0  7580  ensn1  7581  en1  7584  2dom  7590  map1  7596  xp1en  7605  endisj  7606  pw2eng  7625  map2xp  7689  limensuci  7695  1sdom  7724  unxpdom2  7730  sucxpdom  7731  isinf  7735  ac6sfi  7766  fodomfi  7801  0fsupp  7853  fi0  7882  oiexg  7963  brwdom  7996  brwdom2  8002  inf3lemb  8045  infeq5i  8056  dfom3  8067  cantnffvalOLD  8085  cantnfvalf  8087  cantnfval2  8091  cantnfle  8093  cantnflt  8094  cantnff  8096  cantnf0  8097  cantnfp1lem1  8100  cantnfp1lem2  8101  cantnfp1lem3  8102  cantnfp1  8103  cantnflem1a  8107  cantnflem1d  8110  cantnflem1  8111  cantnflem3  8113  cantnf  8115  cantnfval2OLD  8121  cantnfltOLD  8124  cantnfp1lem3OLD  8128  cantnflem1dOLD  8133  cantnflem1OLD  8134  cantnfOLD  8137  cnfcomlem  8146  cnfcom  8147  cnfcom2lem  8148  cnfcom3  8151  cnfcomOLD  8155  tc0  8181  r10  8189  scottex  8306  infxpenlem  8394  fseqenlem1  8408  uncdadom  8554  cdaun  8555  cdaen  8556  cda1dif  8559  pm110.643  8560  cda0en  8562  cdacomen  8564  cdaassen  8565  xpcdaen  8566  mapcdaen  8567  cdaxpdom  8572  cdainf  8575  infcda1  8576  pwsdompw  8587  pwcdadom  8599  ackbij1lem14  8616  ackbij2lem2  8623  ackbij2lem3  8624  cf0  8634  cfeq0  8639  cfsuc  8640  cflim2  8646  isfin5  8682  isfin4-3  8698  fin1a2lem11  8793  fin1a2lem12  8794  fin1a2lem13  8795  axcc2lem  8819  ac6num  8862  zornn0g  8888  ttukeylem3  8894  brdom3  8909  iundom2g  8918  cardeq0  8930  alephadd  8955  pwcfsdom  8961  axpowndlem3  8978  axpowndlem3OLD  8979  canthwe  9032  canthp1lem1  9033  pwxpndom2  9046  pwcdandom  9048  gchxpidm  9050  intwun  9116  0tsk  9136  grothomex  9210  indpi  9288  fzennn  12059  hash0  12418  hashen1  12420  hashmap  12474  hashbc  12483  hashf1  12487  hashge3el3dif  12505  swrdval  12625  swrd00  12626  swrd0  12639  cshfn  12742  cshnz  12744  0csh0  12745  incexclem  13629  incexc  13630  rexpen  13942  sadcf  14084  sadc0  14085  sadcp1  14086  smupf  14109  smup0  14110  smupp1  14111  0ram  14519  ram0  14521  cshws0  14567  str0  14651  ressbas  14668  ress0  14672  0rest  14808  xpscg  14936  xpscfn  14937  xpsc0  14938  xpsc1  14939  xpsfrnel  14941  xpsfrnel2  14943  xpsle  14959  ismred2  14981  acsfn  15037  0cat  15066  setcepi  15393  0pos  15562  meet0  15745  join0  15746  gsum0  15883  ga0  16314  psgn0fv0  16514  pmtrsn  16522  oppglsm  16640  efgi0  16716  vrgpf  16764  vrgpinv  16765  frgpuptinv  16767  frgpup2  16772  0frgp  16775  frgpnabllem1  16855  frgpnabllem2  16856  dprd0  17056  dmdprdpr  17076  dprdpr  17077  00lsp  17605  fvcoe1  18224  coe1f2  18226  coe1sfi  18230  coe1sfiOLD  18231  coe1add  18283  coe1mul2lem1  18286  coe1mul2lem2  18287  coe1mul2  18288  ply1coe  18315  ply1coeOLD  18316  evls1rhmlem  18336  evl1sca  18348  evl1var  18350  pf1mpf  18366  pf1ind  18369  frgpcyg  18589  frlmiscvec  18861  mat0dimscm  18948  mat0dimcrng  18949  mat0scmat  19017  mavmul0  19031  mavmul0g  19032  mvmumamul1  19033  mdet0pr  19071  mdet0f1o  19072  mdet0fv0  19073  mdetunilem9  19099  d0mat2pmat  19216  chpmat0d  19312  topgele  19412  en1top  19463  en2top  19464  sn0topon  19476  indistopon  19479  indistps  19489  indistps2  19490  sn0cld  19568  indiscld  19569  neipeltop  19607  rest0  19647  restsn  19648  cmpfi  19885  refun0  19993  txindislem  20111  hmphindis  20275  xpstopnlem1  20287  xpstopnlem2  20289  ptcmpfi  20291  snfil  20342  fbasfip  20346  fgcl  20356  filcon  20361  fbasrn  20362  cfinfil  20371  csdfil  20372  supfil  20373  ufildr  20409  fin1aufil  20410  rnelfmlem  20430  fclsval  20486  tmdgsum  20571  tsmsfbas  20603  ust0  20699  ustn0  20700  0met  20846  xpsdsval  20861  minveclem3b  21820  tdeglem2  22436  deg1ldg  22469  deg1leb  22472  deg1val  22473  deg1valOLD  22474  ulm0  22762  uhgra0  24285  uhgra0v  24286  umgra0  24301  usgra0  24346  usgra0v  24347  cusgra0v  24436  cusgra1v  24437  uvtx01vtx  24468  0wlk  24523  0trl  24524  0wlkon  24525  0trlon  24526  0pth  24548  0spth  24549  0pthon  24557  0pthonv  24559  0crct  24602  0cycl  24603  0conngra  24650  0clwlk  24741  vdgr0  24876  0egra0rgra  24912  0vgrargra  24913  frgra0v  24969  2spot0  25040  disjdifprg  27412  fpwrelmapffslem  27531  resvsca  27797  locfinref  27821  esumnul  28036  prsiga  28108  oms0  28243  eulerpartgbij  28288  eulerpartlemmf  28291  derang0  28590  indispcon  28656  rdgprc  29202  dfrdg3  29204  trpredpred  29286  trpred0  29294  nosgnn0  29393  nodense  29424  fullfunfnv  29571  fullfunfv  29572  rank0  29802  ssoninhaus  29888  onint1  29889  heibor1lem  30280  heiborlem6  30287  reheibor  30310  mzpcompact2lem  30659  wopprc  30947  pw2f1ocnv  30954  pwslnmlem0  31012  fnchoice  31358  0cnf  31586  afv0fv0  32072  lincval0  32751  lco0  32763  linds0  32801  bnj941  33564  bnj97  33657  bnj149  33666  bnj150  33667  bnj944  33729  bj-1ex  34255  bj-0nel1  34257  bj-xpnzex  34264  bj-eltag  34283  bj-0eltag  34284  bj-tagss  34286  bj-pr1val  34310  bj-nuliota  34334  bj-nuliotaALT  34335