Theorem 0ex 4211

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 4210. (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 4210	. . 3 |- E. x A. y -. y e. x
2		eq0 3510	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1651	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 146	. 2 |- E. x x = (/)
5	4	issetri 2809	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1393   = wceq 1395   E.wex 1538   e. wcel 2200   _Vcvv 2799   (/)c0 3491

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-nul 4210

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199  df-nul 3492

This theorem is referenced by:  0elpw  4248  0nep0  4249  iin0r  4253  intv  4254  snexprc  4270  p0ex  4272  undifexmid  4277  exmidexmid  4280  ss1o0el1  4281  exmidsssn  4286  exmidel  4289  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  0elon  4483  onm  4492  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmidlem1  4620  onsucelsucexmid  4622  regexmidlem1  4625  reg2exmidlema  4626  ordsoexmid  4654  0elsucexmid  4657  ordpwsucexmid  4662  ordtri2or2exmid  4663  ontri2orexmidim  4664  dcextest  4673  peano1  4686  finds  4692  finds2  4693  0elnn  4711  opthprc  4770  nfunv  5351  fun0  5379  acexmidlema  5992  acexmidlemb  5993  acexmidlemab  5995  ovprc  6037  1st0  6290  2nd0  6291  brtpos0  6398  reldmtpos  6399  tfr0dm  6468  rdg0  6533  frec0g  6543  1n0  6578  el1o  6583  0lt2o  6587  fnom  6596  omexg  6597  om0  6604  nnsucsssuc  6638  mapdm0  6810  map0e  6833  0elixp  6876  en0  6947  ensn1  6948  en1  6951  2dom  6958  map1  6965  rex2dom  6971  dom1o  6977  xp1en  6982  endisj  6983  dom0  6999  php5dom  7024  ssfilem  7037  ssfiexmid  7038  domfiexmid  7040  diffitest  7049  ac6sfi  7060  exmidpw  7070  exmidpw2en  7074  unfiexmid  7080  fi0  7142  djuexb  7211  djulclr  7216  djulcl  7218  djulclb  7222  djulf1or  7223  djulf1o  7225  inl11  7232  djuss  7237  1stinl  7241  2ndinl  7242  0ct  7274  finomni  7307  exmidomni  7309  pr2cv1  7368  exmidonfinlem  7371  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidaclem  7390  dju0en  7396  djucomen  7398  djuassen  7399  xpdjuen  7400  pw1dom2  7412  pw1ne1  7414  fmelpw1o  7432  indpi  7529  frecfzennn  10648  fihashen1  11021  hashunlem  11026  zfz1iso  11063  lswex  11123  s1prc  11156  ccat1st1st  11172  swrdval  11180  swrd0g  11192  pfxval  11206  pfx0g  11208  fnpfx  11209  swrdccat3blem  11271  ennnfonelemj0  12972  ennnfonelem0  12976  ennnfonelemhom  12986  strsl0  13081  fnpr2ob  13373  xpsfrnel  13377  0g0  13409  gsum0g  13429  topgele  14703  en1top  14751  sn0topon  14762  sn0cld  14811  rest0  14853  restsn  14854  0met  15058  vtxval0  15854  iedgval0  15855  uhgr0  15885  upgr0eop  15922  djulclALT  16165  bj-charfun  16170  bj-d0clsepcl  16288  bj-indint  16294  bj-bdfindis  16310  bj-inf2vnlem1  16333  pw1map  16361  pwle2  16364  pw1nct  16369  0nninf  16370  nninfsellemdc  16376  nnnninfex  16388