Theorem 0ex 4417

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 4416. (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 4416	. . 3 |- E. x A. y -. y e. x
2		eq0 3647	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1634	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 209	. 2 |- E. x x = (/)
5	4	issetri 2974	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1367   = wceq 1369   E.wex 1586   e. wcel 1756   _Vcvv 2967   (/)c0 3632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-nul 4416

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2969  df-dif 3326  df-nul 3633

This theorem is referenced by:  sseliALT  4418  csbexg  4419  unisn2  4423  class2set  4454  0elpw  4456  0nep0  4458  unidif0  4460  iin0  4461  notzfaus  4462  intv  4463  snexALT  4473  p0ex  4474  dtruALT  4519  zfpair  4524  snex  4528  dtruALT2  4531  opex  4551  opthwiener  4588  0elon  4767  nsuceq0  4794  snsn0non  4832  opthprc  4881  dmsnsnsn  5312  iotaex  5393  nfunv  5444  fun0  5470  fvrn0  5707  fvssunirn  5708  fprg  5886  ovima0  6237  onint0  6402  tfinds2  6469  finds  6497  finds2  6499  xpexr  6513  soex  6516  supp0  6690  fvn0elsupp  6701  brtpos0  6747  reldmtpos  6748  tfrlem16  6844  tz7.44-1  6854  seqomlem1  6897  1n0  6927  el1o  6931  om0  6949  map0e  7242  ixpexg  7279  0elixp  7286  en0  7364  ensn1  7365  en1  7368  2dom  7374  map1  7380  xp1en  7389  endisj  7390  pw2eng  7409  map2xp  7473  limensuci  7479  1sdom  7507  unxpdom2  7513  sucxpdom  7514  isinf  7518  ac6sfi  7548  fodomfi  7582  0fsupp  7634  fi0  7662  oiexg  7741  brwdom  7774  brwdom2  7780  inf3lemb  7823  infeq5i  7834  dfom3  7845  cantnffvalOLD  7863  cantnfvalf  7865  cantnfval2  7869  cantnfle  7871  cantnflt  7872  cantnff  7874  cantnf0  7875  cantnfp1lem1  7878  cantnfp1lem2  7879  cantnfp1lem3  7880  cantnfp1  7881  cantnflem1a  7885  cantnflem1d  7888  cantnflem1  7889  cantnflem3  7891  cantnf  7893  cantnfval2OLD  7899  cantnfltOLD  7902  cantnfp1lem3OLD  7906  cantnflem1dOLD  7911  cantnflem1OLD  7912  cantnfOLD  7915  cnfcomlem  7924  cnfcom  7925  cnfcom2lem  7926  cnfcom3  7929  cnfcomOLD  7933  tc0  7959  r10  7967  scottex  8084  infxpenlem  8172  fseqenlem1  8186  uncdadom  8332  cdaun  8333  cdaen  8334  cda1dif  8337  pm110.643  8338  cda0en  8340  cdacomen  8342  cdaassen  8343  xpcdaen  8344  mapcdaen  8345  cdaxpdom  8350  cdainf  8353  infcda1  8354  pwsdompw  8365  pwcdadom  8377  ackbij1lem14  8394  ackbij2lem2  8401  ackbij2lem3  8402  cf0  8412  cfeq0  8417  cfsuc  8418  cflim2  8424  isfin5  8460  isfin4-3  8476  fin1a2lem11  8571  fin1a2lem12  8572  fin1a2lem13  8573  axcc2lem  8597  ac6num  8640  zornn0g  8666  ttukeylem3  8672  brdom3  8687  iundom2g  8696  cardeq0  8708  alephadd  8733  pwcfsdom  8739  axpowndlem3  8756  axpowndlem3OLD  8757  canthwe  8810  canthp1lem1  8811  pwxpndom2  8824  pwcdandom  8826  gchxpidm  8828  intwun  8894  0tsk  8914  grothomex  8988  indpi  9068  fzennn  11782  hash0  12127  hashge3el3dif  12179  hashmap  12189  hashbc  12198  hashf1  12202  swrdval  12305  swrd00  12306  swrd0  12319  cshfn  12419  cshnz  12421  0csh0  12422  incexclem  13291  incexc  13292  rexpen  13502  sadcf  13641  sadc0  13642  sadcp1  13643  smupf  13666  smup0  13667  smupp1  13668  0ram  14073  ram0  14075  cshws0  14120  str0  14204  ressbas  14220  ress0  14224  0rest  14360  xpscg  14488  xpscfn  14489  xpsc0  14490  xpsc1  14491  xpsfrnel  14493  xpsfrnel2  14495  xpsle  14511  ismred2  14533  acsfn  14589  0cat  14618  setcepi  14948  0pos  15116  meet0  15299  join0  15300  gsum0  15501  ga0  15807  psgn0fv0  16008  oppglsm  16132  efgi0  16208  vrgpf  16256  vrgpinv  16257  frgpuptinv  16259  frgpup2  16264  0frgp  16267  frgpnabllem1  16342  frgpnabllem2  16343  dprd0  16518  dmdprdpr  16538  dprdpr  16539  00lsp  17042  fvcoe1  17643  coe1f2  17645  coe1sfi  17648  coe1sfiOLD  17649  coe1add  17698  coe1mul2lem1  17701  coe1mul2lem2  17702  coe1mul2  17703  ply1coe  17726  ply1coeOLD  17727  evls1rhmlem  17736  evl1sca  17748  evl1var  17750  pf1mpf  17766  pf1ind  17769  frgpcyg  17986  frlmiscvec  18258  mavmul0  18343  mavmul0g  18344  mvmumamul1  18345  mdet0pr  18383  mdet0f1o  18384  mdet0fv0  18385  mdetunilem9  18406  topgele  18519  en1top  18569  en2top  18570  sn0topon  18582  indistopon  18585  indistps  18595  indistps2  18596  sn0cld  18674  indiscld  18675  neipeltop  18713  rest0  18753  restsn  18754  cmpfi  18991  txindislem  19186  hmphindis  19350  xpstopnlem1  19362  xpstopnlem2  19364  ptcmpfi  19366  snfil  19417  fbasfip  19421  fgcl  19431  filcon  19436  fbasrn  19437  cfinfil  19446  csdfil  19447  supfil  19448  ufildr  19484  fin1aufil  19485  rnelfmlem  19505  fclsval  19561  tmdgsum  19646  tsmsfbas  19678  ust0  19774  ustn0  19775  0met  19921  xpsdsval  19936  minveclem3b  20895  tdeglem2  21510  deg1ldg  21543  deg1leb  21546  deg1val  21547  deg1valOLD  21548  ulm0  21836  uhgra0  23211  uhgra0v  23212  umgra0  23227  usgra0  23257  usgra0v  23258  cusgra0v  23336  cusgra1v  23337  uvtx01vtx  23368  0wlk  23412  0trl  23413  0wlkon  23414  0trlon  23415  0pth  23437  0spth  23438  0pthon  23446  0pthonv  23448  0crct  23480  0cycl  23481  0conngra  23528  vdgr0  23538  disjdifprg  25887  fpwrelmapffslem  26000  resvsca  26267  esumnul  26471  prsiga  26543  oms0  26679  eulerpartgbij  26724  eulerpartlemmf  26727  derang0  27026  indispcon  27092  rdgprc  27577  dfrdg3  27579  trpredpred  27661  trpred0  27669  nosgnn0  27768  nodense  27799  fullfunfnv  27946  fullfunfv  27947  rank0  28177  ssoninhaus  28264  onint1  28265  heibor1lem  28679  heiborlem6  28686  reheibor  28709  mzpcompact2lem  29059  wopprc  29350  pw2f1ocnv  29357  pwslnmlem0  29415  fnchoice  29722  afv0fv0  30026  0clwlk  30399  0egra0rgra  30520  0vgrargra  30521  frgra0v  30556  2spot0  30628  hashen1  30707  pmtrsn  30739  mat0dimscm  30825  mat0dimcrng  30826  lincval0  30880  lco0  30892  linds0  30930  bnj941  31695  bnj97  31788  bnj149  31797  bnj150  31798  bnj944  31860  bj-1ex  32342  bj-0nel1  32344  bj-xpnzex  32351  bj-eltag  32370  bj-0eltag  32371  bj-tagss  32373  bj-pr1val  32397