Theorem 0ex 4299

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 4298. (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 4298	. . 3 |- E. x A. y -. y e. x
2		eq0 3602	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1589	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 201	. 2 |- E. x x = (/)
5	4	issetri 2923	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1546   E.wex 1547   = wceq 1649   e. wcel 1721   _Vcvv 2916   (/)c0 3588

This theorem is referenced by:  class2set  4327  0elpw  4329  0nep0  4330  unidif0  4332  iin0  4333  notzfaus  4334  intv  4335  snexALT  4345  p0ex  4346  dtruALT  4356  zfpair  4361  snex  4365  dtruALT2  4368  opex  4387  opthwiener  4418  0elon  4594  nsuceq0  4621  snsn0non  4659  unisn2  4670  onint0  4735  tfinds2  4802  finds  4830  finds2  4832  opthprc  4884  xpexr  5266  soex  5278  dmsnsnsn  5307  iotaex  5394  nfunv  5443  fun0  5467  fvrn0  5712  fvssunirn  5713  fprg  5874  brtpos0  6445  reldmtpos  6446  tfrlem16  6613  tz7.44-1  6623  seqomlem1  6666  1n0  6698  el1o  6702  om0  6720  map0e  7010  ixpexg  7045  0elixp  7052  en0  7129  ensn1  7130  en1  7133  2dom  7138  map1  7144  xp1en  7153  endisj  7154  pw2eng  7173  map2xp  7236  limensuci  7242  1sdom  7270  unxpdom2  7276  sucxpdom  7277  isinf  7281  ac6sfi  7310  fodomfi  7344  fi0  7383  oiexg  7460  brwdom  7491  brwdom2  7497  inf3lemb  7536  infeq5i  7547  dfom3  7558  cantnfvalf  7576  cantnfval2  7580  cantnflt  7583  cantnff  7585  cantnf0  7586  cantnfp1lem3  7592  cantnflem1d  7600  cantnflem1  7601  cantnf  7605  cnfcom  7613  tc0  7642  r10  7650  scottex  7765  infxpenlem  7851  fseqenlem1  7861  uncdadom  8007  cdaun  8008  cdaen  8009  cda1dif  8012  pm110.643  8013  cda0en  8015  cdacomen  8017  cdaassen  8018  xpcdaen  8019  mapcdaen  8020  cdaxpdom  8025  cdainf  8028  infcda1  8029  pwsdompw  8040  pwcdadom  8052  ackbij1lem14  8069  ackbij2lem2  8076  ackbij2lem3  8077  cf0  8087  cfeq0  8092  cfsuc  8093  cflim2  8099  isfin5  8135  isfin4-3  8151  fin1a2lem11  8246  fin1a2lem12  8247  fin1a2lem13  8248  axcc2lem  8272  ac6num  8315  zornn0g  8341  ttukeylem3  8347  brdom3  8362  iundom2g  8371  cardeq0  8383  alephadd  8408  pwcfsdom  8414  axpowndlem3  8430  canthwe  8482  canthp1lem1  8483  pwxpndom2  8496  pwcdandom  8498  gchxpidm  8500  intwun  8566  0tsk  8586  grothomex  8660  indpi  8740  fzennn  11262  hash0  11601  hashmap  11653  hashbc  11657  hashf1  11661  swrdval  11719  swrd00  11720  incexclem  12571  incexc  12572  rexpen  12782  sadcf  12920  sadc0  12921  sadcp1  12922  smupf  12945  smup0  12946  smupp1  12947  0ram  13343  ram0  13345  str0  13460  ressbas  13474  ress0  13478  0rest  13612  xpscg  13738  xpscfn  13739  xpsc0  13740  xpsc1  13741  xpsfrnel  13743  xpsfrnel2  13745  xpsle  13761  ismred2  13783  acsfn  13839  0cat  13868  setcepi  14198  0pos  14366  meet0  14519  join0  14520  gsum0  14735  ga0  15030  oppglsm  15231  efgi0  15307  vrgpf  15355  vrgpinv  15356  frgpuptinv  15358  frgpup2  15363  0frgp  15366  frgpnabllem1  15439  frgpnabllem2  15440  dprd0  15544  dmdprdpr  15562  dprdpr  15563  00lsp  16012  fvcoe1  16560  coe1f2  16562  coe1sfi  16565  coe1add  16612  coe1mul2lem1  16615  coe1mul2lem2  16616  coe1mul2  16617  ply1coe  16639  frgpcyg  16809  topgele  16954  en1top  17004  en2top  17005  sn0topon  17017  indistopon  17020  indistps  17030  indistps2  17031  sn0cld  17109  indiscld  17110  neipeltop  17148  rest0  17187  restsn  17188  cmpfi  17425  txindislem  17618  hmphindis  17782  xpstopnlem1  17794  xpstopnlem2  17796  ptcmpfi  17798  snfil  17849  fbasfip  17853  fgcl  17863  filcon  17868  fbasrn  17869  filuni  17870  cfinfil  17878  csdfil  17879  supfil  17880  ufildr  17916  fin1aufil  17917  rnelfmlem  17937  fclsval  17993  tmdgsum  18078  tsmsfbas  18110  ust0  18202  ustn0  18203  0met  18349  xpsdsval  18364  minveclem3b  19282  evl1rhm  19902  evl1sca  19903  evl1var  19905  pf1mpf  19925  pf1ind  19928  tdeglem2  19937  deg1ldg  19968  deg1leb  19971  deg1val  19972  ulm0  20260  uhgra0  21297  uhgra0v  21298  umgra0  21313  usgra0  21343  usgra0v  21344  cusgra0v  21422  cusgra1v  21423  uvtx01vtx  21454  0wlk  21498  0trl  21499  0wlkon  21500  0trlon  21501  0pth  21523  0spth  21524  0pthon  21532  0pthonv  21534  0crct  21566  0cycl  21567  0conngra  21614  vdgr0  21624  disjdifprg  23970  esumnul  24396  prsiga  24467  derang0  24808  indispcon  24874  rdgprc  25365  dfrdg3  25367  trpredpred  25445  trpred0  25453  nosgnn0  25526  nodense  25557  fullfunfnv  25699  fullfunfv  25700  rank0  26015  ssoninhaus  26102  onint1  26103  heibor1lem  26408  heiborlem6  26415  reheibor  26438  mzpcompact2lem  26698  wopprc  26991  pw2f1ocnv  26998  pwslnmlem0  27061  fnchoice  27567  afv0fv0  27880  swrd0  28002  frgra0v  28097  2spot0  28167  bnj941  28849  bnj97  28943  bnj149  28952  bnj150  28953  bnj944  29015

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-nul 3589