Theorem 0ex 4221

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 4220. (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 4220	. . 3 |- E. x A. y -. y e. x
2		eq0 3515	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1654	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 146	. 2 |- E. x x = (/)
5	4	issetri 2813	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1396   = wceq 1398   E.wex 1541   e. wcel 2202   _Vcvv 2803   (/)c0 3496

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-nul 4220

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-dif 3203  df-nul 3497

This theorem is referenced by:  0elpw  4260  0nep0  4261  iin0r  4265  intv  4266  snexprc  4282  p0ex  4284  undifexmid  4289  exmidexmid  4292  ss1o0el1  4293  exmidsssn  4298  exmidel  4301  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  0elon  4495  onm  4504  ordtriexmidlem2  4624  ordtriexmid  4625  ontriexmidim  4626  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmidlem1  4632  onsucelsucexmid  4634  regexmidlem1  4637  reg2exmidlema  4638  ordsoexmid  4666  0elsucexmid  4669  ordpwsucexmid  4674  ordtri2or2exmid  4675  ontri2orexmidim  4676  dcextest  4685  peano1  4698  finds  4704  finds2  4705  0elnn  4723  opthprc  4783  nfunv  5366  fun0  5395  acexmidlema  6019  acexmidlemb  6020  acexmidlemab  6022  ovprc  6064  1st0  6316  2nd0  6317  supp0  6416  fvn0elsupp  6429  fvn0elsuppb  6430  brtpos0  6461  reldmtpos  6462  tfr0dm  6531  rdg0  6596  frec0g  6606  2oex  6642  1n0  6643  el1o  6648  0lt2o  6652  fnom  6661  omexg  6662  om0  6669  nnsucsssuc  6703  mapdm0  6875  map0e  6898  0elixp  6941  en0  7012  ensn1  7013  en1  7016  2dom  7023  map1  7030  rex2dom  7039  dom1o  7045  xp1en  7050  endisj  7051  dom0  7067  php5dom  7092  ssfilem  7105  ssfiexmid  7106  ssfilemd  7107  ssfiexmidt  7108  domfiexmid  7110  diffitest  7119  ac6sfi  7130  exmidpw  7143  exmidpw2en  7147  unfiexmid  7153  0fsupp  7223  fi0  7234  djuexb  7303  djulclr  7308  djulcl  7310  djulclb  7314  djulf1or  7315  djulf1o  7317  inl11  7324  djuss  7329  1stinl  7333  2ndinl  7334  0ct  7366  finomni  7399  exmidomni  7401  pr2cv1  7460  exmidonfinlem  7464  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidaclem  7483  dju0en  7489  djucomen  7491  djuassen  7492  xpdjuen  7493  pw1dom2  7505  pw1ne1  7507  indpi  7622  frecfzennn  10751  fihashen1  11124  hashunlem  11130  zfz1iso  11168  lswex  11231  s1prc  11266  ccat1st1st  11284  swrdval  11295  swrd0g  11307  pfxval  11321  pfx0g  11323  fnpfx  11324  swrdccat3blem  11386  fzf1o  12016  ennnfonelemj0  13102  ennnfonelem0  13106  ennnfonelemhom  13116  strsl0  13211  fnpr2ob  13503  xpsfrnel  13507  0g0  13539  gsum0g  13559  topgele  14840  en1top  14888  sn0topon  14899  sn0cld  14948  rest0  14990  restsn  14991  0met  15195  vtxval0  15994  iedgval0  15995  uhgr0  16026  upgr0eop  16063  usgr0  16180  usgr0eop  16183  griedg0prc  16191  0grsubgr  16205  clwwlk0on0  16372  konigsberglem1  16429  konigsberglem2  16430  konigsberglem3  16431  djulclALT  16519  bj-charfun  16523  bj-d0clsepcl  16641  bj-indint  16647  bj-bdfindis  16663  bj-inf2vnlem1  16686  pw1map  16717  pwle2  16720  pw1nct  16725  0nninf  16730  nninfsellemdc  16736  nnnninfex  16748