Theorem 0ex 4410

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 4409. (Contributed by NM, 5-Aug-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 4409	. . 3 |- E. x A. y -. y e. x
2		eq0 3640	. . . 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 2969	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1360   = wceq 1362   E.wex 1589   e. wcel 1755   _Vcvv 2962   (/)c0 3625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-nul 4409

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-nul 3626

This theorem is referenced by:  sseliALT  4411  csbexg  4412  unisn2  4416  class2set  4447  0elpw  4449  0nep0  4451  unidif0  4453  iin0  4454  notzfaus  4455  intv  4456  snexALT  4466  p0ex  4467  dtruALT  4512  zfpair  4517  snex  4521  dtruALT2  4524  opex  4544  opthwiener  4581  0elon  4759  nsuceq0  4786  snsn0non  4824  opthprc  4873  dmsnsnsn  5305  iotaex  5386  nfunv  5437  fun0  5463  fvrn0  5700  fvssunirn  5701  fprg  5878  ovima0  6231  onint0  6396  tfinds2  6463  finds  6491  finds2  6493  xpexr  6507  soex  6510  supp0  6684  fvn0elsupp  6695  brtpos0  6741  reldmtpos  6742  tfrlem16  6838  tz7.44-1  6848  seqomlem1  6891  1n0  6923  el1o  6927  om0  6945  map0e  7238  ixpexg  7275  0elixp  7282  en0  7360  ensn1  7361  en1  7364  2dom  7370  map1  7376  xp1en  7385  endisj  7386  pw2eng  7405  map2xp  7469  limensuci  7475  1sdom  7503  unxpdom2  7509  sucxpdom  7510  isinf  7514  ac6sfi  7544  fodomfi  7578  0fsupp  7630  fi0  7658  oiexg  7737  brwdom  7770  brwdom2  7776  inf3lemb  7819  infeq5i  7830  dfom3  7841  cantnffvalOLD  7859  cantnfvalf  7861  cantnfval2  7865  cantnfle  7867  cantnflt  7868  cantnff  7870  cantnf0  7871  cantnfp1lem1  7874  cantnfp1lem2  7875  cantnfp1lem3  7876  cantnfp1  7877  cantnflem1a  7881  cantnflem1d  7884  cantnflem1  7885  cantnflem3  7887  cantnf  7889  cantnfval2OLD  7895  cantnfltOLD  7898  cantnfp1lem3OLD  7902  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnfOLD  7911  cnfcomlem  7920  cnfcom  7921  cnfcom2lem  7922  cnfcom3  7925  cnfcomOLD  7929  tc0  7955  r10  7963  scottex  8080  infxpenlem  8168  fseqenlem1  8182  uncdadom  8328  cdaun  8329  cdaen  8330  cda1dif  8333  pm110.643  8334  cda0en  8336  cdacomen  8338  cdaassen  8339  xpcdaen  8340  mapcdaen  8341  cdaxpdom  8346  cdainf  8349  infcda1  8350  pwsdompw  8361  pwcdadom  8373  ackbij1lem14  8390  ackbij2lem2  8397  ackbij2lem3  8398  cf0  8408  cfeq0  8413  cfsuc  8414  cflim2  8420  isfin5  8456  isfin4-3  8472  fin1a2lem11  8567  fin1a2lem12  8568  fin1a2lem13  8569  axcc2lem  8593  ac6num  8636  zornn0g  8662  ttukeylem3  8668  brdom3  8683  iundom2g  8692  cardeq0  8704  alephadd  8729  pwcfsdom  8735  axpowndlem3  8752  axpowndlem3OLD  8753  canthwe  8806  canthp1lem1  8807  pwxpndom2  8820  pwcdandom  8822  gchxpidm  8824  intwun  8890  0tsk  8910  grothomex  8984  indpi  9064  fzennn  11774  hash0  12119  hashge3el3dif  12171  hashmap  12181  hashbc  12190  hashf1  12194  swrdval  12297  swrd00  12298  swrd0  12311  cshfn  12411  cshnz  12413  0csh0  12414  incexclem  13282  incexc  13283  rexpen  13493  sadcf  13632  sadc0  13633  sadcp1  13634  smupf  13657  smup0  13658  smupp1  13659  0ram  14064  ram0  14066  cshws0  14111  str0  14195  ressbas  14211  ress0  14215  0rest  14351  xpscg  14479  xpscfn  14480  xpsc0  14481  xpsc1  14482  xpsfrnel  14484  xpsfrnel2  14486  xpsle  14502  ismred2  14524  acsfn  14580  0cat  14609  setcepi  14939  0pos  15107  meet0  15290  join0  15291  gsum0  15490  ga0  15796  psgn0fv0  15997  oppglsm  16121  efgi0  16197  vrgpf  16245  vrgpinv  16246  frgpuptinv  16248  frgpup2  16253  0frgp  16256  frgpnabllem1  16331  frgpnabllem2  16332  dprd0  16502  dmdprdpr  16522  dprdpr  16523  00lsp  16984  fvcoe1  17562  coe1f2  17564  coe1sfi  17567  coe1sfiOLD  17568  coe1add  17616  coe1mul2lem1  17619  coe1mul2lem2  17620  coe1mul2  17621  ply1coe  17643  frgpcyg  17848  frlmiscvec  18120  mavmul0  18205  mavmul0g  18206  mvmumamul1  18207  mdet0pr  18245  mdet0f1o  18246  mdet0fv0  18247  mdetunilem9  18268  topgele  18381  en1top  18431  en2top  18432  sn0topon  18444  indistopon  18447  indistps  18457  indistps2  18458  sn0cld  18536  indiscld  18537  neipeltop  18575  rest0  18615  restsn  18616  cmpfi  18853  txindislem  19048  hmphindis  19212  xpstopnlem1  19224  xpstopnlem2  19226  ptcmpfi  19228  snfil  19279  fbasfip  19283  fgcl  19293  filcon  19298  fbasrn  19299  cfinfil  19308  csdfil  19309  supfil  19310  ufildr  19346  fin1aufil  19347  rnelfmlem  19367  fclsval  19423  tmdgsum  19508  tsmsfbas  19540  ust0  19636  ustn0  19637  0met  19783  xpsdsval  19798  minveclem3b  20757  evl1rhm  21380  evl1sca  21381  evl1var  21383  pf1mpf  21403  pf1ind  21406  tdeglem2  21415  deg1ldg  21448  deg1leb  21451  deg1val  21452  deg1valOLD  21453  ulm0  21741  uhgra0  23066  uhgra0v  23067  umgra0  23082  usgra0  23112  usgra0v  23113  cusgra0v  23191  cusgra1v  23192  uvtx01vtx  23223  0wlk  23267  0trl  23268  0wlkon  23269  0trlon  23270  0pth  23292  0spth  23293  0pthon  23301  0pthonv  23303  0crct  23335  0cycl  23336  0conngra  23383  vdgr0  23393  disjdifprg  25743  resvsca  26152  esumnul  26356  prsiga  26428  derang0  26905  indispcon  26971  rdgprc  27455  dfrdg3  27457  trpredpred  27539  trpred0  27547  nosgnn0  27646  nodense  27677  fullfunfnv  27824  fullfunfv  27825  rank0  28055  ssoninhaus  28142  onint1  28143  heibor1lem  28552  heiborlem6  28559  reheibor  28582  mzpcompact2lem  28933  wopprc  29224  pw2f1ocnv  29231  pwslnmlem0  29289  fnchoice  29596  afv0fv0  29901  0clwlk  30274  0egra0rgra  30395  0vgrargra  30396  frgra0v  30431  2spot0  30503  hashen1  30581  pmtrsn  30601  mat0dimscm  30645  mat0dimcrng  30646  lincval0  30658  lco0  30670  linds0  30708  bnj941  31468  bnj97  31561  bnj149  31570  bnj150  31571  bnj944  31633  bj-1ex  32025  bj-0nel1  32027  bj-xpnzex  32034  bj-eltag  32053  bj-0eltag  32054  bj-tagss  32056  bj-pr1val  32080