Theorem 0ex 3987

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 3986. (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 3986	. . 3 |- E. x A. y -. y e. x
2		eq0 3320	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1548	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 145	. 2 |- E. x x = (/)
5	4	issetri 2642	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1294   = wceq 1296   E.wex 1433   e. wcel 1445   _Vcvv 2633   (/)c0 3302

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-nul 3986

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-dif 3015  df-nul 3303

This theorem is referenced by:  0elpw  4020  0nep0  4021  iin0r  4025  intv  4026  snexprc  4042  p0ex  4044  undifexmid  4049  exmidexmid  4052  exmid01  4053  exmidsssn  4055  exmidel  4057  exmidundif  4058  exmidundifim  4059  0elon  4243  onm  4252  ordtriexmidlem2  4365  ordtriexmid  4366  ordtri2orexmid  4367  ontr2exmid  4369  onsucsssucexmid  4371  onsucelsucexmidlem1  4372  onsucelsucexmid  4374  regexmidlem1  4377  reg2exmidlema  4378  ordsoexmid  4406  0elsucexmid  4409  ordpwsucexmid  4414  ordtri2or2exmid  4415  dcextest  4424  peano1  4437  finds  4443  finds2  4444  0elnn  4460  opthprc  4518  nfunv  5081  fun0  5106  acexmidlema  5681  acexmidlemb  5682  acexmidlemab  5684  ovprc  5722  1st0  5953  2nd0  5954  brtpos0  6055  reldmtpos  6056  tfr0dm  6125  rdg0  6190  frec0g  6200  1n0  6235  el1o  6239  0lt2o  6243  fnom  6251  omexg  6252  om0  6259  nnsucsssuc  6293  mapdm0  6460  map0e  6483  0elixp  6526  en0  6592  ensn1  6593  en1  6596  2dom  6602  map1  6609  xp1en  6619  endisj  6620  dom0  6634  php5dom  6659  ssfilem  6671  ssfiexmid  6672  domfiexmid  6674  diffitest  6683  ac6sfi  6694  exmidpw  6704  unfiexmid  6708  djulclr  6821  djulcl  6823  djulclb  6827  djulf1or  6828  djulf1o  6830  djur  6837  djuss  6841  1stinl  6845  2ndinl  6846  0ct  6869  finomni  6883  exmidomni  6885  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  indpi  6998  frecfzennn  9982  fihashen1  10338  hashunlem  10343  zfz1iso  10377  strsl0  11707  topgele  11895  en1top  11945  sn0topon  11956  sn0cld  12005  rest0  12047  restsn  12048  0met  12186  djulclALT  12425  bj-d0clsepcl  12544  bj-indint  12550  bj-bdfindis  12566  bj-inf2vnlem1  12589  pw1dom2  12611  0nninf  12614  nninfsellemdc  12623