Theorem 0ex 4569

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 4568. (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 4568	. . 3 |- E. x A. y -. y e. x
2		eq0 3799	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1672	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 209	. 2 |- E. x x = (/)
5	4	issetri 3113	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1396   = wceq 1398   E.wex 1617   e. wcel 1823   _Vcvv 3106   (/)c0 3783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-nul 3784

This theorem is referenced by:  sseliALT  4570  csbexg  4571  unisn2  4573  class2set  4604  0elpw  4606  0nep0  4608  unidif0  4610  iin0  4611  notzfaus  4612  intv  4613  snexALT  4623  p0ex  4624  dtruALT  4669  zfpair  4674  snex  4678  dtruALT2  4681  opex  4701  opthwiener  4738  0elon  4920  nsuceq0  4947  snsn0non  4985  opthprc  5036  dmsnsnsn  5469  iotaex  5551  nfunv  5601  fun0  5627  fvrn0  5870  fvssunirn  5871  fprg  6056  ovima0  6427  onint0  6604  tfinds2  6671  finds  6699  finds2  6701  xpexr  6713  soex  6716  supp0  6896  fvn0elsupp  6907  fvn0elsuppOLD  6908  fvn0elsuppb  6909  brtpos0  6954  reldmtpos  6955  tfrlem16  7054  tz7.44-1  7064  seqomlem1  7107  1n0  7137  el1o  7141  om0  7159  map0e  7449  ixpexg  7486  0elixp  7493  en0  7571  ensn1  7572  en1  7575  2dom  7581  map1  7587  xp1en  7596  endisj  7597  pw2eng  7616  map2xp  7680  limensuci  7686  1sdom  7715  unxpdom2  7721  sucxpdom  7722  isinf  7726  ac6sfi  7756  fodomfi  7791  0fsupp  7843  fi0  7872  oiexg  7952  brwdom  7985  brwdom2  7991  inf3lemb  8033  infeq5i  8044  dfom3  8055  cantnffvalOLD  8073  cantnfvalf  8075  cantnfval2  8079  cantnfle  8081  cantnflt  8082  cantnff  8084  cantnf0  8085  cantnfp1lem1  8088  cantnfp1lem2  8089  cantnfp1lem3  8090  cantnfp1  8091  cantnflem1a  8095  cantnflem1d  8098  cantnflem1  8099  cantnflem3  8101  cantnf  8103  cantnfval2OLD  8109  cantnfltOLD  8112  cantnfp1lem3OLD  8116  cantnflem1dOLD  8121  cantnflem1OLD  8122  cantnfOLD  8125  cnfcomlem  8134  cnfcom  8135  cnfcom2lem  8136  cnfcom3  8139  cnfcomOLD  8143  tc0  8169  r10  8177  scottex  8294  infxpenlem  8382  fseqenlem1  8396  uncdadom  8542  cdaun  8543  cdaen  8544  cda1dif  8547  pm110.643  8548  cda0en  8550  cdacomen  8552  cdaassen  8553  xpcdaen  8554  mapcdaen  8555  cdaxpdom  8560  cdainf  8563  infcda1  8564  pwsdompw  8575  pwcdadom  8587  ackbij1lem14  8604  ackbij2lem2  8611  ackbij2lem3  8612  cf0  8622  cfeq0  8627  cfsuc  8628  cflim2  8634  isfin5  8670  isfin4-3  8686  fin1a2lem11  8781  fin1a2lem12  8782  fin1a2lem13  8783  axcc2lem  8807  ac6num  8850  zornn0g  8876  ttukeylem3  8882  brdom3  8897  iundom2g  8906  cardeq0  8918  alephadd  8943  pwcfsdom  8949  axpowndlem3  8965  canthwe  9018  canthp1lem1  9019  pwxpndom2  9032  pwcdandom  9034  gchxpidm  9036  intwun  9102  0tsk  9122  grothomex  9196  indpi  9274  fzennn  12063  hash0  12423  hashen1  12425  hashmap  12480  hashbc  12489  hashf1  12493  hashge3el3dif  12511  swrdval  12636  swrd00  12637  swrd0  12653  cshfn  12755  cshnz  12757  0csh0  12758  incexclem  13733  incexc  13734  rexpen  14048  sadcf  14190  sadc0  14191  sadcp1  14192  smupf  14215  smup0  14216  smupp1  14217  0ram  14625  ram0  14627  cshws0  14673  str0  14759  ressbas  14776  ress0  14780  0rest  14922  xpscg  15050  xpscfn  15051  xpsc0  15052  xpsc1  15053  xpsfrnel  15055  xpsfrnel2  15057  xpsle  15073  ismred2  15095  acsfn  15151  0cat  15180  ciclcl  15293  cicrcl  15294  cicer  15297  setcepi  15569  0pos  15786  meet0  15969  join0  15970  gsum0  16107  ga0  16538  psgn0fv0  16738  pmtrsn  16746  oppglsm  16864  efgi0  16940  vrgpf  16988  vrgpinv  16989  frgpuptinv  16991  frgpup2  16996  0frgp  16999  frgpnabllem1  17079  frgpnabllem2  17080  dprd0  17276  dmdprdpr  17296  dprdpr  17297  00lsp  17825  fvcoe1  18444  coe1f2  18446  coe1sfi  18450  coe1sfiOLD  18451  coe1add  18503  coe1mul2lem1  18506  coe1mul2lem2  18507  coe1mul2  18508  ply1coe  18535  ply1coeOLD  18536  evls1rhmlem  18556  evl1sca  18568  evl1var  18570  pf1mpf  18586  pf1ind  18589  frgpcyg  18788  frlmiscvec  19054  mat0dimscm  19141  mat0dimcrng  19142  mat0scmat  19210  mavmul0  19224  mavmul0g  19225  mvmumamul1  19226  mdet0pr  19264  mdet0f1o  19265  mdet0fv0  19266  mdetunilem9  19292  d0mat2pmat  19409  chpmat0d  19505  topgele  19605  en1top  19656  en2top  19657  sn0topon  19669  indistopon  19672  indistps  19682  indistps2  19683  sn0cld  19761  indiscld  19762  neipeltop  19800  rest0  19840  restsn  19841  cmpfi  20078  refun0  20185  txindislem  20303  hmphindis  20467  xpstopnlem1  20479  xpstopnlem2  20481  ptcmpfi  20483  snfil  20534  fbasfip  20538  fgcl  20548  filcon  20553  fbasrn  20554  cfinfil  20563  csdfil  20564  supfil  20565  ufildr  20601  fin1aufil  20602  rnelfmlem  20622  fclsval  20678  tmdgsum  20763  tsmsfbas  20795  ust0  20891  ustn0  20892  0met  21038  xpsdsval  21053  minveclem3b  22012  tdeglem2  22628  deg1ldg  22661  deg1leb  22664  deg1val  22665  deg1valOLD  22666  ulm0  22955  uhgra0  24514  uhgra0v  24515  umgra0  24530  usgra0  24575  usgra0v  24576  cusgra0v  24665  cusgra1v  24666  uvtx01vtx  24697  0wlk  24752  0trl  24753  0wlkon  24754  0trlon  24755  0pth  24777  0spth  24778  0pthon  24786  0pthonv  24788  0crct  24831  0cycl  24832  0conngra  24879  0clwlk  24970  vdgr0  25105  0egra0rgra  25141  0vgrargra  25142  frgra0v  25198  2spot0  25269  disjdifprg  27649  disjun0  27668  fpwrelmapffslem  27789  resvsca  28058  locfinref  28082  esumnul  28280  esumrnmpt2  28300  prsiga  28364  oms0  28508  carsggect  28529  eulerpartgbij  28578  eulerpartlemmf  28581  derang0  28880  indispcon  28946  rdgprc  29470  dfrdg3  29472  trpredpred  29554  trpred0  29562  nosgnn0  29661  nodense  29692  fullfunfnv  29827  fullfunfv  29828  rank0  30058  ssoninhaus  30144  onint1  30145  heibor1lem  30548  heiborlem6  30555  reheibor  30578  mzpcompact2lem  30926  wopprc  31214  pw2f1ocnv  31221  pwslnmlem0  31279  pwfi2f1o  31286  fnchoice  31647  0cnf  31921  dvnprodlem3  31987  afv0fv0  32476  lincval0  33289  lco0  33301  linds0  33339  bnj941  34251  bnj97  34344  bnj149  34353  bnj150  34354  bnj944  34416  bj-1ex  34927  bj-0nel1  34929  bj-xpnzex  34936  bj-eltag  34955  bj-0eltag  34956  bj-tagss  34958  bj-pr1val  34982  bj-nuliota  35006  bj-nuliotaALT  35007