Theorem 0ex 4577

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 4576. (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 4576	. . 3 |- E. x A. y -. y e. x
2		eq0 3800	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1644	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 209	. 2 |- E. x x = (/)
5	4	issetri 3120	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1377   = wceq 1379   E.wex 1596   e. wcel 1767   _Vcvv 3113   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-nul 3786

This theorem is referenced by:  sseliALT  4578  csbexg  4579  unisn2  4583  class2set  4614  0elpw  4616  0nep0  4618  unidif0  4620  iin0  4621  notzfaus  4622  intv  4623  snexALT  4633  p0ex  4634  dtruALT  4679  zfpair  4684  snex  4688  dtruALT2  4691  opex  4711  opthwiener  4749  0elon  4931  nsuceq0  4958  snsn0non  4996  opthprc  5047  dmsnsnsn  5486  iotaex  5568  nfunv  5619  fun0  5645  fvrn0  5888  fvssunirn  5889  fprg  6070  ovima0  6438  onint0  6615  tfinds2  6682  finds  6710  finds2  6712  xpexr  6724  soex  6727  supp0  6906  fvn0elsupp  6917  brtpos0  6962  reldmtpos  6963  tfrlem16  7062  tz7.44-1  7072  seqomlem1  7115  1n0  7145  el1o  7149  om0  7167  map0e  7456  ixpexg  7493  0elixp  7500  en0  7578  ensn1  7579  en1  7582  2dom  7588  map1  7594  xp1en  7603  endisj  7604  pw2eng  7623  map2xp  7687  limensuci  7693  1sdom  7722  unxpdom2  7728  sucxpdom  7729  isinf  7733  ac6sfi  7764  fodomfi  7799  0fsupp  7851  fi0  7880  oiexg  7960  brwdom  7993  brwdom2  7999  inf3lemb  8042  infeq5i  8053  dfom3  8064  cantnffvalOLD  8082  cantnfvalf  8084  cantnfval2  8088  cantnfle  8090  cantnflt  8091  cantnff  8093  cantnf0  8094  cantnfp1lem1  8097  cantnfp1lem2  8098  cantnfp1lem3  8099  cantnfp1  8100  cantnflem1a  8104  cantnflem1d  8107  cantnflem1  8108  cantnflem3  8110  cantnf  8112  cantnfval2OLD  8118  cantnfltOLD  8121  cantnfp1lem3OLD  8125  cantnflem1dOLD  8130  cantnflem1OLD  8131  cantnfOLD  8134  cnfcomlem  8143  cnfcom  8144  cnfcom2lem  8145  cnfcom3  8148  cnfcomOLD  8152  tc0  8178  r10  8186  scottex  8303  infxpenlem  8391  fseqenlem1  8405  uncdadom  8551  cdaun  8552  cdaen  8553  cda1dif  8556  pm110.643  8557  cda0en  8559  cdacomen  8561  cdaassen  8562  xpcdaen  8563  mapcdaen  8564  cdaxpdom  8569  cdainf  8572  infcda1  8573  pwsdompw  8584  pwcdadom  8596  ackbij1lem14  8613  ackbij2lem2  8620  ackbij2lem3  8621  cf0  8631  cfeq0  8636  cfsuc  8637  cflim2  8643  isfin5  8679  isfin4-3  8695  fin1a2lem11  8790  fin1a2lem12  8791  fin1a2lem13  8792  axcc2lem  8816  ac6num  8859  zornn0g  8885  ttukeylem3  8891  brdom3  8906  iundom2g  8915  cardeq0  8927  alephadd  8952  pwcfsdom  8958  axpowndlem3  8975  axpowndlem3OLD  8976  canthwe  9029  canthp1lem1  9030  pwxpndom2  9043  pwcdandom  9045  gchxpidm  9047  intwun  9113  0tsk  9133  grothomex  9207  indpi  9285  fzennn  12046  hash0  12405  hashen1  12407  hashmap  12459  hashbc  12468  hashf1  12472  hashge3el3dif  12490  swrdval  12607  swrd00  12608  swrd0  12621  cshfn  12724  cshnz  12726  0csh0  12727  incexclem  13611  incexc  13612  rexpen  13822  sadcf  13962  sadc0  13963  sadcp1  13964  smupf  13987  smup0  13988  smupp1  13989  0ram  14397  ram0  14399  cshws0  14444  str0  14528  ressbas  14545  ress0  14549  0rest  14685  xpscg  14813  xpscfn  14814  xpsc0  14815  xpsc1  14816  xpsfrnel  14818  xpsfrnel2  14820  xpsle  14836  ismred2  14858  acsfn  14914  0cat  14943  setcepi  15273  0pos  15441  meet0  15624  join0  15625  gsum0  15832  ga0  16141  psgn0fv0  16342  pmtrsn  16350  oppglsm  16468  efgi0  16544  vrgpf  16592  vrgpinv  16593  frgpuptinv  16595  frgpup2  16600  0frgp  16603  frgpnabllem1  16680  frgpnabllem2  16681  dprd0  16880  dmdprdpr  16900  dprdpr  16901  00lsp  17427  fvcoe1  18045  coe1f2  18047  coe1sfi  18051  coe1sfiOLD  18052  coe1add  18104  coe1mul2lem1  18107  coe1mul2lem2  18108  coe1mul2  18109  ply1coe  18136  ply1coeOLD  18137  evls1rhmlem  18157  evl1sca  18169  evl1var  18171  pf1mpf  18187  pf1ind  18190  frgpcyg  18407  frlmiscvec  18679  mat0dimscm  18766  mat0dimcrng  18767  mat0scmat  18835  mavmul0  18849  mavmul0g  18850  mvmumamul1  18851  mdet0pr  18889  mdet0f1o  18890  mdet0fv0  18891  mdetunilem9  18917  d0mat2pmat  19034  chpmat0d  19130  topgele  19230  en1top  19280  en2top  19281  sn0topon  19293  indistopon  19296  indistps  19306  indistps2  19307  sn0cld  19385  indiscld  19386  neipeltop  19424  rest0  19464  restsn  19465  cmpfi  19702  txindislem  19897  hmphindis  20061  xpstopnlem1  20073  xpstopnlem2  20075  ptcmpfi  20077  snfil  20128  fbasfip  20132  fgcl  20142  filcon  20147  fbasrn  20148  cfinfil  20157  csdfil  20158  supfil  20159  ufildr  20195  fin1aufil  20196  rnelfmlem  20216  fclsval  20272  tmdgsum  20357  tsmsfbas  20389  ust0  20485  ustn0  20486  0met  20632  xpsdsval  20647  minveclem3b  21606  tdeglem2  22222  deg1ldg  22255  deg1leb  22258  deg1val  22259  deg1valOLD  22260  ulm0  22548  uhgra0  24013  uhgra0v  24014  umgra0  24029  usgra0  24074  usgra0v  24075  cusgra0v  24164  cusgra1v  24165  uvtx01vtx  24196  0wlk  24251  0trl  24252  0wlkon  24253  0trlon  24254  0pth  24276  0spth  24277  0pthon  24285  0pthonv  24287  0crct  24330  0cycl  24331  0conngra  24378  0clwlk  24469  vdgr0  24604  0egra0rgra  24640  0vgrargra  24641  frgra0v  24697  2spot0  24769  disjdifprg  27137  fpwrelmapffslem  27255  resvsca  27511  esumnul  27727  prsiga  27799  oms0  27934  eulerpartgbij  27979  eulerpartlemmf  27982  derang0  28281  indispcon  28347  rdgprc  28832  dfrdg3  28834  trpredpred  28916  trpred0  28924  nosgnn0  29023  nodense  29054  fullfunfnv  29201  fullfunfv  29202  rank0  29432  ssoninhaus  29518  onint1  29519  heibor1lem  29936  heiborlem6  29943  reheibor  29966  mzpcompact2lem  30316  wopprc  30604  pw2f1ocnv  30611  pwslnmlem0  30669  fnchoice  31010  0cnf  31243  afv0fv0  31729  lincval0  32115  lco0  32127  linds0  32165  bnj941  32928  bnj97  33021  bnj149  33030  bnj150  33031  bnj944  33093  bj-1ex  33606  bj-0nel1  33608  bj-xpnzex  33615  bj-eltag  33634  bj-0eltag  33635  bj-tagss  33637  bj-pr1val  33661  bj-nuliota  33685  bj-nuliotaALT  33686