Theorem 0ex 4499

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 4498. (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 4498	. . 3 |- E. x A. y -. y e. x
2		eq0 3720	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1712	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 212	. 2 |- E. x x = (/)
5	4	issetri 3029	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1435   = wceq 1437   E.wex 1657   e. wcel 1872   _Vcvv 3022   (/)c0 3704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-nul 4498

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-v 3024  df-dif 3382  df-nul 3705

This theorem is referenced by:  sseliALT  4500  csbexg  4501  unisn2  4503  class2set  4534  0elpw  4536  0nep0  4538  unidif0  4540  iin0  4541  notzfaus  4542  intv  4543  snexALT  4553  p0ex  4554  dtruALT  4596  zfpair  4601  snex  4605  dtruALT2  4608  opex  4628  opthwiener  4665  opthprc  4844  dmsnsnsn  5276  0elon  5438  nsuceq0  5465  snsn0non  5503  iotaex  5525  nfunv  5575  fun0  5601  fvrn0  5847  fvssunirn  5848  fprg  6032  ovima0  6406  onint0  6581  tfinds2  6648  finds  6677  finds2  6679  xpexr  6691  soex  6694  supp0  6874  fvn0elsupp  6885  fvn0elsuppOLD  6886  fvn0elsuppb  6887  brtpos0  6935  reldmtpos  6936  tfrlem16  7066  tz7.44-1  7079  seqomlem1  7122  1n0  7152  el1o  7156  om0  7174  map0e  7464  ixpexg  7501  0elixp  7508  en0  7586  ensn1  7587  en1  7590  2dom  7596  map1  7602  xp1en  7611  endisj  7612  pw2eng  7631  map2xp  7695  limensuci  7701  1sdom  7728  unxpdom2  7733  sucxpdom  7734  isinf  7738  ac6sfi  7768  fodomfi  7803  0fsupp  7858  fi0  7887  oiexg  8003  brwdom  8035  brwdom2  8041  inf3lemb  8083  infeq5i  8094  dfom3  8105  cantnfvalf  8122  cantnfval2  8126  cantnfle  8128  cantnflt  8129  cantnff  8131  cantnf0  8132  cantnfp1lem1  8135  cantnfp1lem2  8136  cantnfp1lem3  8137  cantnfp1  8138  cantnflem1a  8142  cantnflem1d  8145  cantnflem1  8146  cantnflem3  8148  cantnf  8150  cnfcomlem  8156  cnfcom  8157  cnfcom2lem  8158  cnfcom3  8161  tc0  8183  r10  8191  scottex  8308  infxpenlem  8396  fseqenlem1  8406  uncdadom  8552  cdaun  8553  cdaen  8554  cda1dif  8557  pm110.643  8558  cda0en  8560  cdacomen  8562  cdaassen  8563  xpcdaen  8564  mapcdaen  8565  cdaxpdom  8570  cdainf  8573  infcda1  8574  pwsdompw  8585  pwcdadom  8597  ackbij1lem14  8614  ackbij2lem2  8621  ackbij2lem3  8622  cf0  8632  cfeq0  8637  cfsuc  8638  cflim2  8644  isfin5  8680  isfin4-3  8696  fin1a2lem11  8791  fin1a2lem12  8792  fin1a2lem13  8793  axcc2lem  8817  ac6num  8860  zornn0g  8886  ttukeylem3  8892  brdom3  8907  iundom2g  8916  cardeq0  8928  alephadd  8953  pwcfsdom  8959  axpowndlem3  8975  canthwe  9027  canthp1lem1  9028  pwxpndom2  9041  pwcdandom  9043  gchxpidm  9045  intwun  9111  0tsk  9131  grothomex  9205  indpi  9283  fzennn  12131  hash0  12498  hashen1  12500  hashmap  12555  hashbc  12564  hashf1  12568  hashge3el3dif  12590  swrdval  12719  swrd00  12720  swrd0  12736  cshfn  12838  cshnz  12840  0csh0  12841  incexclem  13837  incexc  13838  rexpen  14223  sadcf  14370  sadc0  14371  sadcp1  14372  smupf  14395  smup0  14396  smupp1  14397  0ram  14921  ram0  14923  cshws0  15015  str0  15104  ressbas  15122  ress0  15126  0rest  15271  xpscg  15407  xpscfn  15408  xpsc0  15409  xpsc1  15410  xpsfrnel  15412  xpsfrnel2  15414  xpsle  15430  ismred2  15452  acsfn  15508  0cat  15537  ciclcl  15650  cicrcl  15651  cicer  15654  setcepi  15926  0pos  16143  meet0  16326  join0  16327  gsum0  16464  ga0  16895  psgn0fv0  17095  pmtrsn  17103  oppglsm  17237  efgi0  17313  vrgpf  17361  vrgpinv  17362  frgpuptinv  17364  frgpup2  17369  0frgp  17372  frgpnabllem1  17452  frgpnabllem2  17453  dprd0  17607  dmdprdpr  17625  dprdpr  17626  00lsp  18147  fvcoe1  18743  coe1f2  18745  coe1sfi  18749  coe1add  18800  coe1mul2lem1  18803  coe1mul2lem2  18804  coe1mul2  18805  ply1coe  18832  ply1coeOLD  18833  evls1rhmlem  18853  evl1sca  18865  evl1var  18867  pf1mpf  18883  pf1ind  18886  frgpcyg  19086  frlmiscvec  19349  mat0dimscm  19436  mat0dimcrng  19437  mat0scmat  19505  mavmul0  19519  mavmul0g  19520  mvmumamul1  19521  mdet0pr  19559  mdet0f1o  19560  mdet0fv0  19561  mdetunilem9  19587  d0mat2pmat  19704  chpmat0d  19800  topgele  19891  en1top  19942  en2top  19943  sn0topon  19955  indistopon  19958  indistps  19968  indistps2  19969  sn0cld  20048  indiscld  20049  neipeltop  20087  rest0  20127  restsn  20128  cmpfi  20365  refun0  20472  txindislem  20590  hmphindis  20754  xpstopnlem1  20766  xpstopnlem2  20768  ptcmpfi  20770  snfil  20821  fbasfip  20825  fgcl  20835  filcon  20840  fbasrn  20841  cfinfil  20850  csdfil  20851  supfil  20852  ufildr  20888  fin1aufil  20889  rnelfmlem  20909  fclsval  20965  tmdgsum  21052  tsmsfbas  21084  ust0  21176  ustn0  21177  0met  21323  xpsdsval  21338  minveclem3b  22312  minveclem3bOLD  22324  tdeglem2  22952  deg1ldg  22983  deg1leb  22986  deg1val  22987  ulm0  23288  uhgra0  24978  uhgra0v  24979  umgra0  24994  usgra0  25039  usgra0v  25040  cusgra0v  25130  cusgra1v  25131  uvtx01vtx  25162  0wlk  25217  0trl  25218  0wlkon  25219  0trlon  25220  0pth  25242  0spth  25243  0pthon  25251  0pthonv  25253  0crct  25296  0cycl  25297  0conngra  25344  0clwlk  25435  vdgr0  25570  0egra0rgra  25606  0vgrargra  25607  frgra0v  25663  2spot0  25734  disjdifprg  28131  disjun0  28151  fpwrelmapffslem  28267  f1ocnt  28326  resvsca  28545  locfinref  28620  esumnul  28821  esumrnmpt2  28841  prsiga  28905  ldsysgenld  28934  oms0  29077  oms0OLD  29081  carsggect  29102  eulerpartgbij  29157  eulerpartlemmf  29160  bnj941  29536  bnj97  29629  bnj149  29638  bnj150  29639  bnj944  29701  derang0  29844  indispcon  29909  rdgprc  30392  dfrdg3  30394  trpredpred  30420  trpred0  30428  nosgnn0  30496  nodense  30527  fullfunfnv  30662  fullfunfv  30663  rank0  30886  ssoninhaus  31057  onint1  31058  bj-1ex  31455  bj-0nel1  31457  bj-xpnzex  31463  bj-eltag  31482  bj-0eltag  31483  bj-tagss  31485  bj-pr1val  31509  bj-nuliota  31533  bj-nuliotaALT  31534  finxpreclem1  31688  finxpreclem2  31689  finxp0  31690  finxpreclem5  31694  poimirlem28  31875  heibor1lem  32048  heiborlem6  32055  reheibor  32078  mzpcompact2lem  35505  wopprc  35798  pw2f1ocnv  35805  pwslnmlem0  35862  pwfi2f1o  35867  relintabex  36100  fnchoice  37266  mapdm0  37375  0cnf  37637  dvnprodlem3  37706  prsal  38043  intsal  38053  sge00  38069  sge0sn  38072  nnfoctbdjlem  38144  isomenndlem  38202  afv0fv0  38464  vtxval0  38914  iedgval0  38915  uhgr0  38941  upgr0eop  38974  upgr0eopALT  38976  usgr0  39072  usgr0eop  39075  0grsubgr  39097  cplgr0  39231  lincval0  39811  lco0  39823  linds0  39861