Theorem 0ex 4145

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 4144. (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 4144	. . 3 |- E. x A. y -. y e. x
2		eq0 3456	. . . 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 2761	1 |- (/) e. _V

Syntax hints:   -. wn 3   A.wal 1362   = wceq 1364   E.wex 1503   e. wcel 2160   _Vcvv 2752   (/)c0 3437

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 2171  ax-nul 4144

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-dif 3146  df-nul 3438

This theorem is referenced by:  0elpw  4182  0nep0  4183  iin0r  4187  intv  4188  snexprc  4204  p0ex  4206  undifexmid  4211  exmidexmid  4214  ss1o0el1  4215  exmidsssn  4220  exmidel  4223  exmidundif  4224  exmidundifim  4225  exmid1stab  4226  0elon  4410  onm  4419  ordtriexmidlem2  4537  ordtriexmid  4538  ontriexmidim  4539  ordtri2orexmid  4540  ontr2exmid  4542  onsucsssucexmid  4544  onsucelsucexmidlem1  4545  onsucelsucexmid  4547  regexmidlem1  4550  reg2exmidlema  4551  ordsoexmid  4579  0elsucexmid  4582  ordpwsucexmid  4587  ordtri2or2exmid  4588  ontri2orexmidim  4589  dcextest  4598  peano1  4611  finds  4617  finds2  4618  0elnn  4636  opthprc  4695  nfunv  5268  fun0  5293  acexmidlema  5887  acexmidlemb  5888  acexmidlemab  5890  ovprc  5931  1st0  6169  2nd0  6170  brtpos0  6277  reldmtpos  6278  tfr0dm  6347  rdg0  6412  frec0g  6422  1n0  6457  el1o  6462  0lt2o  6466  fnom  6475  omexg  6476  om0  6483  nnsucsssuc  6517  mapdm0  6689  map0e  6712  0elixp  6755  en0  6821  ensn1  6822  en1  6825  2dom  6831  map1  6838  xp1en  6849  endisj  6850  dom0  6866  php5dom  6891  ssfilem  6903  ssfiexmid  6904  domfiexmid  6906  diffitest  6915  ac6sfi  6926  exmidpw  6936  exmidpw2en  6940  unfiexmid  6946  fi0  7004  djuexb  7073  djulclr  7078  djulcl  7080  djulclb  7084  djulf1or  7085  djulf1o  7087  inl11  7094  djuss  7099  1stinl  7103  2ndinl  7104  0ct  7136  finomni  7168  exmidomni  7170  exmidonfinlem  7222  exmidfodomrlemr  7231  exmidfodomrlemrALT  7232  exmidaclem  7237  dju0en  7243  djucomen  7245  djuassen  7246  xpdjuen  7247  pw1dom2  7256  pw1ne1  7258  indpi  7371  frecfzennn  10457  fihashen1  10811  hashunlem  10816  zfz1iso  10853  ennnfonelemj0  12452  ennnfonelem0  12456  ennnfonelemhom  12466  strsl0  12561  fnpr2ob  12816  xpsfrnel  12820  0g0  12852  topgele  13986  en1top  14034  sn0topon  14045  sn0cld  14094  rest0  14136  restsn  14137  0met  14341  djulclALT  15011  fmelpw1o  15016  bj-charfun  15017  bj-d0clsepcl  15135  bj-indint  15141  bj-bdfindis  15157  bj-inf2vnlem1  15180  pwle2  15207  pw1nct  15211  0nninf  15212  nninfsellemdc  15218