Theorem 0ex 4171

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 4170. (Contributed by NM, 5-Aug-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 4170	. . 3 |- E. x A. y -. y e. x
2		eq0 3479	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1628	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 146	. 2 |- E. x x = (/)
5	4	issetri 2781	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1371   = wceq 1373   E.wex 1515   e. wcel 2176   _Vcvv 2772   (/)c0 3460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-nul 4170

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-dif 3168  df-nul 3461

This theorem is referenced by:  0elpw  4208  0nep0  4209  iin0r  4213  intv  4214  snexprc  4230  p0ex  4232  undifexmid  4237  exmidexmid  4240  ss1o0el1  4241  exmidsssn  4246  exmidel  4249  exmidundif  4250  exmidundifim  4251  exmid1stab  4252  0elon  4439  onm  4448  ordtriexmidlem2  4568  ordtriexmid  4569  ontriexmidim  4570  ordtri2orexmid  4571  ontr2exmid  4573  onsucsssucexmid  4575  onsucelsucexmidlem1  4576  onsucelsucexmid  4578  regexmidlem1  4581  reg2exmidlema  4582  ordsoexmid  4610  0elsucexmid  4613  ordpwsucexmid  4618  ordtri2or2exmid  4619  ontri2orexmidim  4620  dcextest  4629  peano1  4642  finds  4648  finds2  4649  0elnn  4667  opthprc  4726  nfunv  5304  fun0  5332  acexmidlema  5935  acexmidlemb  5936  acexmidlemab  5938  ovprc  5980  1st0  6230  2nd0  6231  brtpos0  6338  reldmtpos  6339  tfr0dm  6408  rdg0  6473  frec0g  6483  1n0  6518  el1o  6523  0lt2o  6527  fnom  6536  omexg  6537  om0  6544  nnsucsssuc  6578  mapdm0  6750  map0e  6773  0elixp  6816  en0  6887  ensn1  6888  en1  6891  2dom  6897  map1  6904  rex2dom  6910  xp1en  6918  endisj  6919  dom0  6935  php5dom  6960  ssfilem  6972  ssfiexmid  6973  domfiexmid  6975  diffitest  6984  ac6sfi  6995  exmidpw  7005  exmidpw2en  7009  unfiexmid  7015  fi0  7077  djuexb  7146  djulclr  7151  djulcl  7153  djulclb  7157  djulf1or  7158  djulf1o  7160  inl11  7167  djuss  7172  1stinl  7176  2ndinl  7177  0ct  7209  finomni  7242  exmidomni  7244  exmidonfinlem  7301  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidaclem  7320  dju0en  7326  djucomen  7328  djuassen  7329  xpdjuen  7330  pw1dom2  7339  pw1ne1  7341  indpi  7455  frecfzennn  10571  fihashen1  10944  hashunlem  10949  zfz1iso  10986  s1prc  11077  ccat1st1st  11093  swrdval  11101  swrd0g  11113  ennnfonelemj0  12772  ennnfonelem0  12776  ennnfonelemhom  12786  strsl0  12881  fnpr2ob  13172  xpsfrnel  13176  0g0  13208  gsum0g  13228  topgele  14501  en1top  14549  sn0topon  14560  sn0cld  14609  rest0  14651  restsn  14652  0met  14856  vtxval0  15648  iedgval0  15649  djulclALT  15737  fmelpw1o  15742  bj-charfun  15743  bj-d0clsepcl  15861  bj-indint  15867  bj-bdfindis  15883  bj-inf2vnlem1  15906  pwle2  15935  pw1nct  15940  0nninf  15941  nninfsellemdc  15947  nnnninfex  15959