Theorem 0ex 4157

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 4156. (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 4156	. . 3 |- E. x A. y -. y e. x
2		eq0 3466	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1616	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 146	. 2 |- E. x x = (/)
5	4	issetri 2769	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1362   = wceq 1364   E.wex 1503   e. wcel 2164   _Vcvv 2760   (/)c0 3447

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-nul 4156

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-dif 3156  df-nul 3448

This theorem is referenced by:  0elpw  4194  0nep0  4195  iin0r  4199  intv  4200  snexprc  4216  p0ex  4218  undifexmid  4223  exmidexmid  4226  ss1o0el1  4227  exmidsssn  4232  exmidel  4235  exmidundif  4236  exmidundifim  4237  exmid1stab  4238  0elon  4424  onm  4433  ordtriexmidlem2  4553  ordtriexmid  4554  ontriexmidim  4555  ordtri2orexmid  4556  ontr2exmid  4558  onsucsssucexmid  4560  onsucelsucexmidlem1  4561  onsucelsucexmid  4563  regexmidlem1  4566  reg2exmidlema  4567  ordsoexmid  4595  0elsucexmid  4598  ordpwsucexmid  4603  ordtri2or2exmid  4604  ontri2orexmidim  4605  dcextest  4614  peano1  4627  finds  4633  finds2  4634  0elnn  4652  opthprc  4711  nfunv  5288  fun0  5313  acexmidlema  5910  acexmidlemb  5911  acexmidlemab  5913  ovprc  5954  1st0  6199  2nd0  6200  brtpos0  6307  reldmtpos  6308  tfr0dm  6377  rdg0  6442  frec0g  6452  1n0  6487  el1o  6492  0lt2o  6496  fnom  6505  omexg  6506  om0  6513  nnsucsssuc  6547  mapdm0  6719  map0e  6742  0elixp  6785  en0  6851  ensn1  6852  en1  6855  2dom  6861  map1  6868  xp1en  6879  endisj  6880  dom0  6896  php5dom  6921  ssfilem  6933  ssfiexmid  6934  domfiexmid  6936  diffitest  6945  ac6sfi  6956  exmidpw  6966  exmidpw2en  6970  unfiexmid  6976  fi0  7036  djuexb  7105  djulclr  7110  djulcl  7112  djulclb  7116  djulf1or  7117  djulf1o  7119  inl11  7126  djuss  7131  1stinl  7135  2ndinl  7136  0ct  7168  finomni  7201  exmidomni  7203  exmidonfinlem  7255  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  dju0en  7276  djucomen  7278  djuassen  7279  xpdjuen  7280  pw1dom2  7289  pw1ne1  7291  indpi  7404  frecfzennn  10500  fihashen1  10873  hashunlem  10878  zfz1iso  10915  ennnfonelemj0  12561  ennnfonelem0  12565  ennnfonelemhom  12575  strsl0  12670  fnpr2ob  12926  xpsfrnel  12930  0g0  12962  gsum0g  12982  topgele  14208  en1top  14256  sn0topon  14267  sn0cld  14316  rest0  14358  restsn  14359  0met  14563  djulclALT  15363  fmelpw1o  15368  bj-charfun  15369  bj-d0clsepcl  15487  bj-indint  15493  bj-bdfindis  15509  bj-inf2vnlem1  15532  pwle2  15559  pw1nct  15563  0nninf  15564  nninfsellemdc  15570