Theorem 0ex 4172

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 4171. (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 4171	. . 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 4171

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  4209  0nep0  4210  iin0r  4214  intv  4215  snexprc  4231  p0ex  4233  undifexmid  4238  exmidexmid  4241  ss1o0el1  4242  exmidsssn  4247  exmidel  4250  exmidundif  4251  exmidundifim  4252  exmid1stab  4253  0elon  4440  onm  4449  ordtriexmidlem2  4569  ordtriexmid  4570  ontriexmidim  4571  ordtri2orexmid  4572  ontr2exmid  4574  onsucsssucexmid  4576  onsucelsucexmidlem1  4577  onsucelsucexmid  4579  regexmidlem1  4582  reg2exmidlema  4583  ordsoexmid  4611  0elsucexmid  4614  ordpwsucexmid  4619  ordtri2or2exmid  4620  ontri2orexmidim  4621  dcextest  4630  peano1  4643  finds  4649  finds2  4650  0elnn  4668  opthprc  4727  nfunv  5305  fun0  5333  acexmidlema  5937  acexmidlemb  5938  acexmidlemab  5940  ovprc  5982  1st0  6232  2nd0  6233  brtpos0  6340  reldmtpos  6341  tfr0dm  6410  rdg0  6475  frec0g  6485  1n0  6520  el1o  6525  0lt2o  6529  fnom  6538  omexg  6539  om0  6546  nnsucsssuc  6580  mapdm0  6752  map0e  6775  0elixp  6818  en0  6889  ensn1  6890  en1  6893  2dom  6899  map1  6906  rex2dom  6912  xp1en  6920  endisj  6921  dom0  6937  php5dom  6962  ssfilem  6974  ssfiexmid  6975  domfiexmid  6977  diffitest  6986  ac6sfi  6997  exmidpw  7007  exmidpw2en  7011  unfiexmid  7017  fi0  7079  djuexb  7148  djulclr  7153  djulcl  7155  djulclb  7159  djulf1or  7160  djulf1o  7162  inl11  7169  djuss  7174  1stinl  7178  2ndinl  7179  0ct  7211  finomni  7244  exmidomni  7246  exmidonfinlem  7303  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidaclem  7322  dju0en  7328  djucomen  7330  djuassen  7331  xpdjuen  7332  pw1dom2  7341  pw1ne1  7343  indpi  7457  frecfzennn  10573  fihashen1  10946  hashunlem  10951  zfz1iso  10988  lswex  11047  s1prc  11080  ccat1st1st  11096  swrdval  11104  swrd0g  11116  pfxval  11130  pfx0g  11132  ennnfonelemj0  12805  ennnfonelem0  12809  ennnfonelemhom  12819  strsl0  12914  fnpr2ob  13205  xpsfrnel  13209  0g0  13241  gsum0g  13261  topgele  14534  en1top  14582  sn0topon  14593  sn0cld  14642  rest0  14684  restsn  14685  0met  14889  vtxval0  15681  iedgval0  15682  djulclALT  15774  fmelpw1o  15779  bj-charfun  15780  bj-d0clsepcl  15898  bj-indint  15904  bj-bdfindis  15920  bj-inf2vnlem1  15943  pwle2  15972  pw1nct  15977  0nninf  15978  nninfsellemdc  15984  nnnninfex  15996