Theorem 0ex 4557

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 4556. (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 4556	. . 3 |- E. x A. y -. y e. x
2		eq0 3783	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1714	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 212	. 2 |- E. x x = (/)
5	4	issetri 3094	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1870   _Vcvv 3087   (/)c0 3767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-v 3089  df-dif 3445  df-nul 3768

This theorem is referenced by:  sseliALT  4558  csbexg  4559  unisn2  4561  class2set  4592  0elpw  4594  0nep0  4596  unidif0  4598  iin0  4599  notzfaus  4600  intv  4601  snexALT  4611  p0ex  4612  dtruALT  4654  zfpair  4659  snex  4663  dtruALT2  4666  opex  4686  opthwiener  4723  opthprc  4902  dmsnsnsn  5334  0elon  5495  nsuceq0  5522  snsn0non  5560  iotaex  5582  nfunv  5632  fun0  5658  fvrn0  5903  fvssunirn  5904  fprg  6088  ovima0  6462  onint0  6637  tfinds2  6704  finds  6733  finds2  6735  xpexr  6747  soex  6750  supp0  6930  fvn0elsupp  6941  fvn0elsuppOLD  6942  fvn0elsuppb  6943  brtpos0  6988  reldmtpos  6989  tfrlem16  7119  tz7.44-1  7132  seqomlem1  7175  1n0  7205  el1o  7209  om0  7227  map0e  7517  ixpexg  7554  0elixp  7561  en0  7639  ensn1  7640  en1  7643  2dom  7649  map1  7655  xp1en  7664  endisj  7665  pw2eng  7684  map2xp  7748  limensuci  7754  1sdom  7781  unxpdom2  7786  sucxpdom  7787  isinf  7791  ac6sfi  7821  fodomfi  7856  0fsupp  7911  fi0  7940  oiexg  8050  brwdom  8082  brwdom2  8088  inf3lemb  8130  infeq5i  8141  dfom3  8152  cantnfvalf  8169  cantnfval2  8173  cantnfle  8175  cantnflt  8176  cantnff  8178  cantnf0  8179  cantnfp1lem1  8182  cantnfp1lem2  8183  cantnfp1lem3  8184  cantnfp1  8185  cantnflem1a  8189  cantnflem1d  8192  cantnflem1  8193  cantnflem3  8195  cantnf  8197  cnfcomlem  8203  cnfcom  8204  cnfcom2lem  8205  cnfcom3  8208  tc0  8230  r10  8238  scottex  8355  infxpenlem  8443  fseqenlem1  8453  uncdadom  8599  cdaun  8600  cdaen  8601  cda1dif  8604  pm110.643  8605  cda0en  8607  cdacomen  8609  cdaassen  8610  xpcdaen  8611  mapcdaen  8612  cdaxpdom  8617  cdainf  8620  infcda1  8621  pwsdompw  8632  pwcdadom  8644  ackbij1lem14  8661  ackbij2lem2  8668  ackbij2lem3  8669  cf0  8679  cfeq0  8684  cfsuc  8685  cflim2  8691  isfin5  8727  isfin4-3  8743  fin1a2lem11  8838  fin1a2lem12  8839  fin1a2lem13  8840  axcc2lem  8864  ac6num  8907  zornn0g  8933  ttukeylem3  8939  brdom3  8954  iundom2g  8963  cardeq0  8975  alephadd  9000  pwcfsdom  9006  axpowndlem3  9022  canthwe  9075  canthp1lem1  9076  pwxpndom2  9089  pwcdandom  9091  gchxpidm  9093  intwun  9159  0tsk  9179  grothomex  9253  indpi  9331  fzennn  12178  hash0  12545  hashen1  12547  hashmap  12602  hashbc  12611  hashf1  12615  hashge3el3dif  12633  swrdval  12758  swrd00  12759  swrd0  12775  cshfn  12877  cshnz  12879  0csh0  12880  incexclem  13872  incexc  13873  rexpen  14258  sadcf  14401  sadc0  14402  sadcp1  14403  smupf  14426  smup0  14427  smupp1  14428  0ram  14941  ram0  14943  cshws0  15035  str0  15124  ressbas  15141  ress0  15145  0rest  15287  xpscg  15415  xpscfn  15416  xpsc0  15417  xpsc1  15418  xpsfrnel  15420  xpsfrnel2  15422  xpsle  15438  ismred2  15460  acsfn  15516  0cat  15545  ciclcl  15658  cicrcl  15659  cicer  15662  setcepi  15934  0pos  16151  meet0  16334  join0  16335  gsum0  16472  ga0  16903  psgn0fv0  17103  pmtrsn  17111  oppglsm  17229  efgi0  17305  vrgpf  17353  vrgpinv  17354  frgpuptinv  17356  frgpup2  17361  0frgp  17364  frgpnabllem1  17444  frgpnabllem2  17445  dprd0  17599  dmdprdpr  17617  dprdpr  17618  00lsp  18139  fvcoe1  18735  coe1f2  18737  coe1sfi  18741  coe1add  18792  coe1mul2lem1  18795  coe1mul2lem2  18796  coe1mul2  18797  ply1coe  18824  ply1coeOLD  18825  evls1rhmlem  18845  evl1sca  18857  evl1var  18859  pf1mpf  18875  pf1ind  18878  frgpcyg  19075  frlmiscvec  19338  mat0dimscm  19425  mat0dimcrng  19426  mat0scmat  19494  mavmul0  19508  mavmul0g  19509  mvmumamul1  19510  mdet0pr  19548  mdet0f1o  19549  mdet0fv0  19550  mdetunilem9  19576  d0mat2pmat  19693  chpmat0d  19789  topgele  19880  en1top  19931  en2top  19932  sn0topon  19944  indistopon  19947  indistps  19957  indistps2  19958  sn0cld  20037  indiscld  20038  neipeltop  20076  rest0  20116  restsn  20117  cmpfi  20354  refun0  20461  txindislem  20579  hmphindis  20743  xpstopnlem1  20755  xpstopnlem2  20757  ptcmpfi  20759  snfil  20810  fbasfip  20814  fgcl  20824  filcon  20829  fbasrn  20830  cfinfil  20839  csdfil  20840  supfil  20841  ufildr  20877  fin1aufil  20878  rnelfmlem  20898  fclsval  20954  tmdgsum  21041  tsmsfbas  21073  ust0  21165  ustn0  21166  0met  21312  xpsdsval  21327  minveclem3b  22263  tdeglem2  22887  deg1ldg  22918  deg1leb  22921  deg1val  22922  ulm0  23211  uhgra0  24882  uhgra0v  24883  umgra0  24898  usgra0  24943  usgra0v  24944  cusgra0v  25033  cusgra1v  25034  uvtx01vtx  25065  0wlk  25120  0trl  25121  0wlkon  25122  0trlon  25123  0pth  25145  0spth  25146  0pthon  25154  0pthonv  25156  0crct  25199  0cycl  25200  0conngra  25247  0clwlk  25338  vdgr0  25473  0egra0rgra  25509  0vgrargra  25510  frgra0v  25566  2spot0  25637  disjdifprg  28024  disjun0  28044  fpwrelmapffslem  28160  f1ocnt  28212  resvsca  28432  locfinref  28507  esumnul  28708  esumrnmpt2  28728  prsiga  28792  ldsysgenld  28821  oms0  28958  carsggect  28979  eulerpartgbij  29031  eulerpartlemmf  29034  bnj941  29372  bnj97  29465  bnj149  29474  bnj150  29475  bnj944  29537  derang0  29680  indispcon  29745  rdgprc  30228  dfrdg3  30230  trpredpred  30256  trpred0  30264  nosgnn0  30332  nodense  30363  fullfunfnv  30498  fullfunfv  30499  rank0  30722  ssoninhaus  30893  onint1  30894  bj-1ex  31293  bj-0nel1  31295  bj-xpnzex  31301  bj-eltag  31320  bj-0eltag  31321  bj-tagss  31323  bj-pr1val  31347  bj-nuliota  31371  bj-nuliotaALT  31372  poimirlem28  31671  heibor1lem  31844  heiborlem6  31851  reheibor  31874  mzpcompact2lem  35301  wopprc  35590  pw2f1ocnv  35597  pwslnmlem0  35654  pwfi2f1o  35659  fnchoice  36989  0cnf  37325  dvnprodlem3  37391  prsal  37725  intsal  37735  sge00  37751  sge0sn  37754  nnfoctbdjlem  37801  afv0fv0  38040  lincval0  38967  lco0  38979  linds0  39017