Theorem 0ex 4160

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 4159. (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 4159	. . 3 |- E. x A. y -. y e. x
2		eq0 3469	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1619	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 146	. 2 |- E. x x = (/)
5	4	issetri 2772	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1362   = wceq 1364   E.wex 1506   e. wcel 2167   _Vcvv 2763   (/)c0 3450

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-nul 4159

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-dif 3159  df-nul 3451

This theorem is referenced by:  0elpw  4197  0nep0  4198  iin0r  4202  intv  4203  snexprc  4219  p0ex  4221  undifexmid  4226  exmidexmid  4229  ss1o0el1  4230  exmidsssn  4235  exmidel  4238  exmidundif  4239  exmidundifim  4240  exmid1stab  4241  0elon  4427  onm  4436  ordtriexmidlem2  4556  ordtriexmid  4557  ontriexmidim  4558  ordtri2orexmid  4559  ontr2exmid  4561  onsucsssucexmid  4563  onsucelsucexmidlem1  4564  onsucelsucexmid  4566  regexmidlem1  4569  reg2exmidlema  4570  ordsoexmid  4598  0elsucexmid  4601  ordpwsucexmid  4606  ordtri2or2exmid  4607  ontri2orexmidim  4608  dcextest  4617  peano1  4630  finds  4636  finds2  4637  0elnn  4655  opthprc  4714  nfunv  5291  fun0  5316  acexmidlema  5913  acexmidlemb  5914  acexmidlemab  5916  ovprc  5957  1st0  6202  2nd0  6203  brtpos0  6310  reldmtpos  6311  tfr0dm  6380  rdg0  6445  frec0g  6455  1n0  6490  el1o  6495  0lt2o  6499  fnom  6508  omexg  6509  om0  6516  nnsucsssuc  6550  mapdm0  6722  map0e  6745  0elixp  6788  en0  6854  ensn1  6855  en1  6858  2dom  6864  map1  6871  xp1en  6882  endisj  6883  dom0  6899  php5dom  6924  ssfilem  6936  ssfiexmid  6937  domfiexmid  6939  diffitest  6948  ac6sfi  6959  exmidpw  6969  exmidpw2en  6973  unfiexmid  6979  fi0  7041  djuexb  7110  djulclr  7115  djulcl  7117  djulclb  7121  djulf1or  7122  djulf1o  7124  inl11  7131  djuss  7136  1stinl  7140  2ndinl  7141  0ct  7173  finomni  7206  exmidomni  7208  exmidonfinlem  7260  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  dju0en  7281  djucomen  7283  djuassen  7284  xpdjuen  7285  pw1dom2  7294  pw1ne1  7296  indpi  7409  frecfzennn  10518  fihashen1  10891  hashunlem  10896  zfz1iso  10933  ennnfonelemj0  12618  ennnfonelem0  12622  ennnfonelemhom  12632  strsl0  12727  fnpr2ob  12983  xpsfrnel  12987  0g0  13019  gsum0g  13039  topgele  14265  en1top  14313  sn0topon  14324  sn0cld  14373  rest0  14415  restsn  14416  0met  14620  djulclALT  15447  fmelpw1o  15452  bj-charfun  15453  bj-d0clsepcl  15571  bj-indint  15577  bj-bdfindis  15593  bj-inf2vnlem1  15616  pwle2  15643  pw1nct  15647  0nninf  15648  nninfsellemdc  15654