Theorem 0ex 4549

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 4548. (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 4548	. . 3 |- E. x A. y -. y e. x
2		eq0 3759	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1729	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 214	. 2 |- E. x x = (/)
5	4	issetri 3064	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1453   = wceq 1455   E.wex 1674   e. wcel 1898   _Vcvv 3057   (/)c0 3743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-nul 4548

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-v 3059  df-dif 3419  df-nul 3744

This theorem is referenced by:  sseliALT  4550  csbexg  4551  unisn2  4553  class2set  4584  0elpw  4586  0nep0  4588  unidif0  4590  iin0  4591  notzfaus  4592  intv  4593  snexALT  4603  p0ex  4604  dtruALT  4646  zfpair  4651  snex  4655  dtruALT2  4658  opex  4678  opthwiener  4717  opthprc  4901  dmsnsnsn  5333  0elon  5495  nsuceq0  5522  snsn0non  5560  iotaex  5582  nfunv  5632  fun0  5661  fvrn0  5910  fvssunirn  5911  fprg  6097  ovima0  6475  onint0  6650  tfinds2  6717  finds  6746  finds2  6748  xpexr  6760  soex  6763  supp0  6946  fvn0elsupp  6957  fvn0elsuppOLD  6958  fvn0elsuppb  6959  brtpos0  7006  reldmtpos  7007  tfrlem16  7137  tz7.44-1  7150  seqomlem1  7193  1n0  7223  el1o  7227  om0  7245  map0e  7535  ixpexg  7572  0elixp  7579  en0  7658  ensn1  7659  en1  7662  2dom  7668  map1  7674  xp1en  7684  endisj  7685  pw2eng  7704  map2xp  7768  limensuci  7774  1sdom  7801  unxpdom2  7806  sucxpdom  7807  isinf  7811  ac6sfi  7841  fodomfi  7876  0fsupp  7931  fi0  7960  oiexg  8076  brwdom  8108  brwdom2  8114  inf3lemb  8156  infeq5i  8167  dfom3  8178  cantnfvalf  8196  cantnfval2  8200  cantnfle  8202  cantnflt  8203  cantnff  8205  cantnf0  8206  cantnfp1lem1  8209  cantnfp1lem2  8210  cantnfp1lem3  8211  cantnfp1  8212  cantnflem1a  8216  cantnflem1d  8219  cantnflem1  8220  cantnflem3  8222  cantnf  8224  cnfcomlem  8230  cnfcom  8231  cnfcom2lem  8232  cnfcom3  8235  tc0  8257  r10  8265  scottex  8382  infxpenlem  8470  fseqenlem1  8481  uncdadom  8627  cdaun  8628  cdaen  8629  cda1dif  8632  pm110.643  8633  cda0en  8635  cdacomen  8637  cdaassen  8638  xpcdaen  8639  mapcdaen  8640  cdaxpdom  8645  cdainf  8648  infcda1  8649  pwsdompw  8660  pwcdadom  8672  ackbij1lem14  8689  ackbij2lem2  8696  ackbij2lem3  8697  cf0  8707  cfeq0  8712  cfsuc  8713  cflim2  8719  isfin5  8755  isfin4-3  8771  fin1a2lem11  8866  fin1a2lem12  8867  fin1a2lem13  8868  axcc2lem  8892  ac6num  8935  zornn0g  8961  ttukeylem3  8967  brdom3  8982  iundom2g  8991  cardeq0  9003  alephadd  9028  pwcfsdom  9034  axpowndlem3  9050  canthwe  9102  canthp1lem1  9103  pwxpndom2  9116  pwcdandom  9118  gchxpidm  9120  intwun  9186  0tsk  9206  grothomex  9280  indpi  9358  fzennn  12213  hash0  12580  hashen1  12582  hashmap  12640  hashbc  12649  hashf1  12653  hashge3el3dif  12675  swrdval  12810  swrd00  12811  swrd0  12827  cshfn  12929  cshnz  12931  0csh0  12932  incexclem  13943  incexc  13944  rexpen  14329  sadcf  14476  sadc0  14477  sadcp1  14478  smupf  14501  smup0  14502  smupp1  14503  0ram  15027  ram0  15029  cshws0  15121  str0  15210  ressbas  15228  ress0  15232  0rest  15377  xpscg  15513  xpscfn  15514  xpsc0  15515  xpsc1  15516  xpsfrnel  15518  xpsfrnel2  15520  xpsle  15536  ismred2  15558  acsfn  15614  0cat  15643  ciclcl  15756  cicrcl  15757  cicer  15760  setcepi  16032  0pos  16249  meet0  16432  join0  16433  gsum0  16570  ga0  17001  psgn0fv0  17201  pmtrsn  17209  oppglsm  17343  efgi0  17419  vrgpf  17467  vrgpinv  17468  frgpuptinv  17470  frgpup2  17475  0frgp  17478  frgpnabllem1  17558  frgpnabllem2  17559  dprd0  17713  dmdprdpr  17731  dprdpr  17732  00lsp  18253  fvcoe1  18849  coe1f2  18851  coe1sfi  18855  coe1add  18906  coe1mul2lem1  18909  coe1mul2lem2  18910  coe1mul2  18911  ply1coe  18938  ply1coeOLD  18939  evls1rhmlem  18959  evl1sca  18971  evl1var  18973  pf1mpf  18989  pf1ind  18992  frgpcyg  19193  frlmiscvec  19456  mat0dimscm  19543  mat0dimcrng  19544  mat0scmat  19612  mavmul0  19626  mavmul0g  19627  mvmumamul1  19628  mdet0pr  19666  mdet0f1o  19667  mdet0fv0  19668  mdetunilem9  19694  d0mat2pmat  19811  chpmat0d  19907  topgele  19998  en1top  20049  en2top  20050  sn0topon  20062  indistopon  20065  indistps  20075  indistps2  20076  sn0cld  20155  indiscld  20156  neipeltop  20194  rest0  20234  restsn  20235  cmpfi  20472  refun0  20579  txindislem  20697  hmphindis  20861  xpstopnlem1  20873  xpstopnlem2  20875  ptcmpfi  20877  snfil  20928  fbasfip  20932  fgcl  20942  filcon  20947  fbasrn  20948  cfinfil  20957  csdfil  20958  supfil  20959  ufildr  20995  fin1aufil  20996  rnelfmlem  21016  fclsval  21072  tmdgsum  21159  tsmsfbas  21191  ust0  21283  ustn0  21284  0met  21430  xpsdsval  21445  minveclem3b  22419  minveclem3bOLD  22431  tdeglem2  23059  deg1ldg  23090  deg1leb  23093  deg1val  23094  ulm0  23395  uhgra0  25085  uhgra0v  25086  umgra0  25101  usgra0  25146  usgra0v  25147  cusgra0v  25237  cusgra1v  25238  uvtx01vtx  25269  0wlk  25324  0trl  25325  0wlkon  25326  0trlon  25327  0pth  25349  0spth  25350  0pthon  25358  0pthonv  25360  0crct  25403  0cycl  25404  0conngra  25451  0clwlk  25542  vdgr0  25677  0egra0rgra  25713  0vgrargra  25714  frgra0v  25770  2spot0  25841  disjdifprg  28234  disjun0  28254  fpwrelmapffslem  28366  f1ocnt  28425  resvsca  28642  locfinref  28717  esumnul  28918  esumrnmpt2  28938  prsiga  29002  ldsysgenld  29031  oms0  29174  oms0OLD  29178  carsggect  29199  eulerpartgbij  29254  eulerpartlemmf  29257  bnj941  29633  bnj97  29726  bnj149  29735  bnj150  29736  bnj944  29798  derang0  29941  indispcon  30006  rdgprc  30490  dfrdg3  30492  trpredpred  30518  trpred0  30526  nosgnn0  30594  nodense  30627  fullfunfnv  30762  fullfunfv  30763  rank0  30986  ssoninhaus  31157  onint1  31158  bj-1ex  31589  bj-0nel1  31591  bj-xpnzex  31597  bj-eltag  31616  bj-0eltag  31617  bj-tagss  31619  bj-pr1val  31643  bj-nuliota  31668  bj-nuliotaALT  31669  finxpreclem1  31826  finxpreclem2  31827  finxp0  31828  finxpreclem5  31832  poimirlem28  32013  heibor1lem  32186  heiborlem6  32193  reheibor  32216  mzpcompact2lem  35638  wopprc  35930  pw2f1ocnv  35937  pwslnmlem0  35994  pwfi2f1o  35999  relintabex  36232  fnchoice  37390  mapdm0  37509  0cnf  37792  dvnprodlem3  37861  qndenserrnbl  38202  prsal  38217  intsal  38227  sge00  38256  sge0sn  38259  nnfoctbdjlem  38331  isomenndlem  38389  hoiqssbl  38485  afv0fv0  38689  vtxval0  39185  iedgval0  39186  uhgr0  39213  upgr0eop  39250  upgr0eopALT  39252  usgr0  39368  usgr0eop  39371  griedg0prc  39386  0grsubgr  39400  cplgr0  39543  0grrusgr  39645  0ewlk  39828  01wlk  39832  0wlkOn  39837  0Trl  39838  0TrlOn  39840  0pth-av  39841  0spth-av  39842  0pthon-av  39843  0pthonv-av  39845  0Crct  39848  0Cycl  39849  0conngr  39933  lincval0  40481  lco0  40493  linds0  40531