Theorem 0ex 4790

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 4789. (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 4789	. . 3 |- E. x A. y -. y e. x
2		eq0 3929	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1774	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 221	. 2 |- E. x x = (/)
5	4	issetri 3210	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  sseliALT  4791  csbexg  4792  unisn2  4794  class2set  4832  0elpw  4834  0nep0  4836  unidif0  4838  iin0  4839  notzfaus  4840  intv  4841  snexALT  4852  p0ex  4853  dtruALT  4899  zfpair  4904  snex  4908  dtruALT2  4911  opex  4932  opthwiener  4976  opthprc  5167  nrelv  5244  dmsnsnsn  5613  0elon  5778  nsuceq0  5805  snsn0non  5846  iotaex  5868  nfunv  5921  fun0  5954  fvrn0  6216  fvssunirn  6217  fprg  6422  ovima0  6813  onint0  6996  tfinds2  7063  finds  7092  finds2  7094  xpexr  7106  soex  7109  supp0  7300  fvn0elsupp  7311  fvn0elsuppb  7312  brtpos0  7359  reldmtpos  7360  tfrlem16  7489  tz7.44-1  7502  seqomlem1  7545  1n0  7575  el1o  7579  om0  7597  mapdm0  7872  map0e  7895  ixpexg  7932  0elixp  7939  en0  8019  ensn1  8020  en1  8023  2dom  8029  map1  8036  xp1en  8046  endisj  8047  pw2eng  8066  map2xp  8130  limensuci  8136  1sdom  8163  unxpdom2  8168  sucxpdom  8169  isinf  8173  ac6sfi  8204  fodomfi  8239  0fsupp  8297  fi0  8326  oiexg  8440  brwdom  8472  brwdom2  8478  inf3lemb  8522  infeq5i  8533  dfom3  8544  cantnfvalf  8562  cantnfval2  8566  cantnfle  8568  cantnflt  8569  cantnff  8571  cantnf0  8572  cantnfp1lem1  8575  cantnfp1lem2  8576  cantnfp1lem3  8577  cantnfp1  8578  cantnflem1a  8582  cantnflem1d  8585  cantnflem1  8586  cantnflem3  8588  cantnf  8590  cnfcomlem  8596  cnfcom  8597  cnfcom2lem  8598  cnfcom3  8601  tc0  8623  r10  8631  scottex  8748  infxpenlem  8836  fseqenlem1  8847  uncdadom  8993  cdaun  8994  cdaen  8995  cda1dif  8998  pm110.643  8999  cda0en  9001  cdacomen  9003  cdaassen  9004  xpcdaen  9005  mapcdaen  9006  cdaxpdom  9011  cdainf  9014  infcda1  9015  pwsdompw  9026  pwcdadom  9038  ackbij1lem14  9055  ackbij2lem2  9062  ackbij2lem3  9063  cf0  9073  cfeq0  9078  cfsuc  9079  cflim2  9085  isfin5  9121  isfin4-3  9137  fin1a2lem11  9232  fin1a2lem12  9233  fin1a2lem13  9234  axcc2lem  9258  ac6num  9301  zornn0g  9327  ttukeylem3  9333  brdom3  9350  iundom2g  9362  cardeq0  9374  alephadd  9399  pwcfsdom  9405  axpowndlem3  9421  canthwe  9473  canthp1lem1  9474  pwxpndom2  9487  pwcdandom  9489  gchxpidm  9491  intwun  9557  0tsk  9577  grothomex  9651  indpi  9729  fzennn  12767  hash0  13158  hashen1  13160  hashmap  13222  hashbc  13237  hashf1  13241  hashge3el3dif  13268  swrdval  13417  swrd00  13418  swrd0  13434  cshfn  13536  cshnz  13538  0csh0  13539  incexclem  14568  incexc  14569  rexpen  14957  sadcf  15175  sadc0  15176  sadcp1  15177  smupf  15200  smup0  15201  smupp1  15202  0ram  15724  ram0  15726  cshws0  15808  str0  15911  ressbas  15930  ress0  15934  0rest  16090  xpscg  16218  xpscfn  16219  xpsc0  16220  xpsc1  16221  xpsfrnel  16223  xpsfrnel2  16225  xpsle  16241  ismred2  16263  acsfn  16320  0cat  16349  ciclcl  16462  cicrcl  16463  cicer  16466  setcepi  16738  0pos  16954  meet0  17137  join0  17138  mgm0b  17256  gsum0  17278  sgrp0b  17292  ga0  17731  psgn0fv0  17931  pmtrsn  17939  oppglsm  18057  efgi0  18133  vrgpf  18181  vrgpinv  18182  frgpuptinv  18184  frgpup2  18189  0frgp  18192  frgpnabllem1  18276  frgpnabllem2  18277  dprd0  18430  dmdprdpr  18448  dprdpr  18449  00lsp  18981  fvcoe1  19577  coe1f2  19579  coe1sfi  19583  coe1add  19634  coe1mul2lem1  19637  coe1mul2lem2  19638  coe1mul2  19639  ply1coe  19666  evls1rhmlem  19686  evl1sca  19698  evl1var  19700  pf1mpf  19716  pf1ind  19719  cnfldfunALT  19759  frgpcyg  19922  frlmiscvec  20188  mat0dimscm  20275  mat0dimcrng  20276  mat0scmat  20344  mavmul0  20358  mavmul0g  20359  mvmumamul1  20360  mdet0pr  20398  mdet0f1o  20399  mdet0fv0  20400  mdetunilem9  20426  d0mat2pmat  20543  chpmat0d  20639  topgele  20734  en1top  20788  en2top  20789  sn0topon  20802  indistopon  20805  indistps  20815  indistps2  20816  sn0cld  20894  indiscld  20895  neipeltop  20933  rest0  20973  restsn  20974  cmpfi  21211  refun0  21318  txindislem  21436  hmphindis  21600  xpstopnlem1  21612  xpstopnlem2  21614  ptcmpfi  21616  snfil  21668  fbasfip  21672  fgcl  21682  filconn  21687  fbasrn  21688  cfinfil  21697  csdfil  21698  supfil  21699  ufildr  21735  fin1aufil  21736  rnelfmlem  21756  fclsval  21812  tmdgsum  21899  tsmsfbas  21931  ust0  22023  ustn0  22024  0met  22171  xpsdsval  22186  minveclem3b  23199  tdeglem2  23821  deg1ldg  23852  deg1leb  23855  deg1val  23856  ulm0  24145  uhgr0  25968  upgr0eop  26009  upgr0eopALT  26011  usgr0  26135  usgr0eop  26138  lfuhgr1v0e  26146  griedg0prc  26156  0grsubgr  26170  cplgr0  26321  0grrusgr  26475  0ewlk  26975  0wlkon  26981  0trlon  26985  0pthon  26988  0pthonv  26990  0conngr  27052  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  disjdifprg  29388  disjun0  29408  fpwrelmapffslem  29507  f1ocnt  29559  resvsca  29830  locfinref  29908  esumnul  30110  esumrnmpt2  30130  prsiga  30194  ldsysgenld  30223  ldgenpisyslem1  30226  oms0  30359  carsggect  30380  eulerpartgbij  30434  eulerpartlemmf  30437  repr0  30689  breprexp  30711  bnj941  30843  bnj97  30936  bnj149  30945  bnj150  30946  bnj944  31008  derang0  31151  indispconn  31216  rdgprc  31700  dfrdg3  31702  trpredpred  31728  trpred0  31736  nosgnn0  31811  nodense  31842  nolt02o  31845  nulsslt  31908  nulssgt  31909  fullfunfnv  32053  fullfunfv  32054  rank0  32277  ssoninhaus  32447  onint1  32448  bj-1ex  32938  bj-0nel1  32940  bj-xpnzex  32946  bj-eltag  32965  bj-0eltag  32966  bj-tagss  32968  bj-pr1val  32992  bj-nuliota  33019  bj-nuliotaALT  33020  bj-rest10  33041  bj-rest10b  33042  bj-rest0  33046  finxpreclem1  33226  finxpreclem2  33227  finxp0  33228  finxpreclem5  33232  poimirlem28  33437  heibor1lem  33608  heiborlem6  33615  reheibor  33638  n0elqs  34098  mzpcompact2lem  37314  wopprc  37597  pw2f1ocnv  37604  pwslnmlem0  37661  pwfi2f1o  37666  relintabex  37887  clsk1indlem0  38339  clsk1indlem4  38342  clsk1indlem1  38343  fnchoice  39188  eliuniincex  39292  mapdm0OLD  39383  limsup0  39926  0cnv  39974  liminf0  40025  0cnf  40090  dvnprodlem3  40163  qndenserrnbl  40515  prsal  40538  intsal  40548  sge00  40593  sge0sn  40596  nnfoctbdjlem  40672  isomenndlem  40744  hoiqssbl  40839  ovnsubadd2lem  40859  afv0fv0  41229  lincval0  42204  lco0  42216  linds0  42254  bnd2d  42428