Theorem 0ex 4529

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 4528. (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 4528	. . 3 |- E. x A. y -. y e. x
2		eq0 3759	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1635	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 209	. 2 |- E. x x = (/)
5	4	issetri 3083	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1368   = wceq 1370   E.wex 1587   e. wcel 1758   _Vcvv 3076   (/)c0 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4528

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-v 3078  df-dif 3438  df-nul 3745

This theorem is referenced by:  sseliALT  4530  csbexg  4531  unisn2  4535  class2set  4566  0elpw  4568  0nep0  4570  unidif0  4572  iin0  4573  notzfaus  4574  intv  4575  snexALT  4585  p0ex  4586  dtruALT  4631  zfpair  4636  snex  4640  dtruALT2  4643  opex  4663  opthwiener  4700  0elon  4879  nsuceq0  4906  snsn0non  4944  opthprc  4993  dmsnsnsn  5424  iotaex  5505  nfunv  5556  fun0  5582  fvrn0  5820  fvssunirn  5821  fprg  5999  ovima0  6351  onint0  6516  tfinds2  6583  finds  6611  finds2  6613  xpexr  6627  soex  6630  supp0  6804  fvn0elsupp  6815  brtpos0  6861  reldmtpos  6862  tfrlem16  6961  tz7.44-1  6971  seqomlem1  7014  1n0  7044  el1o  7048  om0  7066  map0e  7359  ixpexg  7396  0elixp  7403  en0  7481  ensn1  7482  en1  7485  2dom  7491  map1  7497  xp1en  7506  endisj  7507  pw2eng  7526  map2xp  7590  limensuci  7596  1sdom  7625  unxpdom2  7631  sucxpdom  7632  isinf  7636  ac6sfi  7666  fodomfi  7700  0fsupp  7752  fi0  7780  oiexg  7859  brwdom  7892  brwdom2  7898  inf3lemb  7941  infeq5i  7952  dfom3  7963  cantnffvalOLD  7981  cantnfvalf  7983  cantnfval2  7987  cantnfle  7989  cantnflt  7990  cantnff  7992  cantnf0  7993  cantnfp1lem1  7996  cantnfp1lem2  7997  cantnfp1lem3  7998  cantnfp1  7999  cantnflem1a  8003  cantnflem1d  8006  cantnflem1  8007  cantnflem3  8009  cantnf  8011  cantnfval2OLD  8017  cantnfltOLD  8020  cantnfp1lem3OLD  8024  cantnflem1dOLD  8029  cantnflem1OLD  8030  cantnfOLD  8033  cnfcomlem  8042  cnfcom  8043  cnfcom2lem  8044  cnfcom3  8047  cnfcomOLD  8051  tc0  8077  r10  8085  scottex  8202  infxpenlem  8290  fseqenlem1  8304  uncdadom  8450  cdaun  8451  cdaen  8452  cda1dif  8455  pm110.643  8456  cda0en  8458  cdacomen  8460  cdaassen  8461  xpcdaen  8462  mapcdaen  8463  cdaxpdom  8468  cdainf  8471  infcda1  8472  pwsdompw  8483  pwcdadom  8495  ackbij1lem14  8512  ackbij2lem2  8519  ackbij2lem3  8520  cf0  8530  cfeq0  8535  cfsuc  8536  cflim2  8542  isfin5  8578  isfin4-3  8594  fin1a2lem11  8689  fin1a2lem12  8690  fin1a2lem13  8691  axcc2lem  8715  ac6num  8758  zornn0g  8784  ttukeylem3  8790  brdom3  8805  iundom2g  8814  cardeq0  8826  alephadd  8851  pwcfsdom  8857  axpowndlem3  8874  axpowndlem3OLD  8875  canthwe  8928  canthp1lem1  8929  pwxpndom2  8942  pwcdandom  8944  gchxpidm  8946  intwun  9012  0tsk  9032  grothomex  9106  indpi  9186  fzennn  11906  hash0  12251  hashen1  12253  hashge3el3dif  12304  hashmap  12314  hashbc  12323  hashf1  12327  swrdval  12430  swrd00  12431  swrd0  12444  cshfn  12544  cshnz  12546  0csh0  12547  incexclem  13416  incexc  13417  rexpen  13627  sadcf  13766  sadc0  13767  sadcp1  13768  smupf  13791  smup0  13792  smupp1  13793  0ram  14198  ram0  14200  cshws0  14245  str0  14329  ressbas  14346  ress0  14350  0rest  14486  xpscg  14614  xpscfn  14615  xpsc0  14616  xpsc1  14617  xpsfrnel  14619  xpsfrnel2  14621  xpsle  14637  ismred2  14659  acsfn  14715  0cat  14744  setcepi  15074  0pos  15242  meet0  15425  join0  15426  gsum0  15628  ga0  15934  psgn0fv0  16135  pmtrsn  16143  oppglsm  16261  efgi0  16337  vrgpf  16385  vrgpinv  16386  frgpuptinv  16388  frgpup2  16393  0frgp  16396  frgpnabllem1  16471  frgpnabllem2  16472  dprd0  16649  dmdprdpr  16669  dprdpr  16670  00lsp  17184  fvcoe1  17786  coe1f2  17788  coe1sfi  17791  coe1sfiOLD  17792  coe1add  17840  coe1mul2lem1  17843  coe1mul2lem2  17844  coe1mul2  17845  ply1coe  17870  ply1coeOLD  17871  evls1rhmlem  17880  evl1sca  17892  evl1var  17894  pf1mpf  17910  pf1ind  17913  frgpcyg  18130  frlmiscvec  18402  mavmul0  18489  mavmul0g  18490  mvmumamul1  18491  mdet0pr  18529  mdet0f1o  18530  mdet0fv0  18531  mdetunilem9  18557  topgele  18670  en1top  18720  en2top  18721  sn0topon  18733  indistopon  18736  indistps  18746  indistps2  18747  sn0cld  18825  indiscld  18826  neipeltop  18864  rest0  18904  restsn  18905  cmpfi  19142  txindislem  19337  hmphindis  19501  xpstopnlem1  19513  xpstopnlem2  19515  ptcmpfi  19517  snfil  19568  fbasfip  19572  fgcl  19582  filcon  19587  fbasrn  19588  cfinfil  19597  csdfil  19598  supfil  19599  ufildr  19635  fin1aufil  19636  rnelfmlem  19656  fclsval  19712  tmdgsum  19797  tsmsfbas  19829  ust0  19925  ustn0  19926  0met  20072  xpsdsval  20087  minveclem3b  21046  tdeglem2  21662  deg1ldg  21695  deg1leb  21698  deg1val  21699  deg1valOLD  21700  ulm0  21988  uhgra0  23394  uhgra0v  23395  umgra0  23410  usgra0  23440  usgra0v  23441  cusgra0v  23519  cusgra1v  23520  uvtx01vtx  23551  0wlk  23595  0trl  23596  0wlkon  23597  0trlon  23598  0pth  23620  0spth  23621  0pthon  23629  0pthonv  23631  0crct  23663  0cycl  23664  0conngra  23711  vdgr0  23721  disjdifprg  26069  fpwrelmapffslem  26182  resvsca  26442  esumnul  26646  prsiga  26718  oms0  26853  eulerpartgbij  26898  eulerpartlemmf  26901  derang0  27200  indispcon  27266  rdgprc  27751  dfrdg3  27753  trpredpred  27835  trpred0  27843  nosgnn0  27942  nodense  27973  fullfunfnv  28120  fullfunfv  28121  rank0  28351  ssoninhaus  28437  onint1  28438  heibor1lem  28855  heiborlem6  28862  reheibor  28885  mzpcompact2lem  29235  wopprc  29526  pw2f1ocnv  29533  pwslnmlem0  29591  fnchoice  29898  afv0fv0  30202  0clwlk  30575  0egra0rgra  30696  0vgrargra  30697  frgra0v  30732  2spot0  30804  mat0dimscm  31030  mat0dimcrng  31031  lincval0  31067  lco0  31079  linds0  31117  d0mat2pmat  31213  cpmat0d  31305  bnj941  32083  bnj97  32176  bnj149  32185  bnj150  32186  bnj944  32248  bj-1ex  32759  bj-0nel1  32761  bj-xpnzex  32768  bj-eltag  32787  bj-0eltag  32788  bj-tagss  32790  bj-pr1val  32814  bj-nuliota  32838  bj-nuliotaALT  32839