Theorem 0ex 4262

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 4261. (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 4261	. . 3 |- E. x A. y -. y e. x
2		eq0 3540	. . . 4 |- ( x = (/) <-> A. y -. y e. x )
3	2	exbii 1658	. . 3 |- ( E. x x = (/) <-> E. x A. y -. y e. x )
4	1, 3	mpbir 146	. 2 |- E. x x = (/)
5	4	issetri 2831	1 |- (/) e. _V

This proof depends on syntax axioms:   -. wn 3   A.wal 1400   = wceq 1402   E.wex 1545   e. wcel 2209   _Vcvv 2821   (/)c0 3520

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-nul 4261

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-dif 3222  df-nul 3521

This theorem is used by:  0elpw  4303  0nep0  4304  iin0r  4308  intv  4309  snexprc  4325  p0ex  4327  undifexmid  4332  exmidexmid  4335  ss1o0el1  4336  exmidsssn  4341  exmidel  4344  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  0elon  4539  onm  4548  ordtriexmidlem2  4669  ordtriexmid  4670  ontriexmidim  4671  ordtri2orexmid  4672  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmidlem1  4677  onsucelsucexmid  4679  regexmidlem1  4682  reg2exmidlema  4683  ordsoexmid  4711  0elsucexmid  4714  ordpwsucexmid  4719  ordtri2or2exmid  4720  ontri2orexmidim  4721  dcextest  4730  peano1  4743  finds  4749  finds2  4750  0elnn  4768  opthprc  4828  nfunv  5413  fun0  5442  acexmidlema  6079  acexmidlemb  6080  acexmidlemab  6082  ovprc  6124  1st0  6382  2nd0  6383  supp0  6482  fvn0elsupp  6495  fvn0elsuppb  6496  brtpos0  6528  reldmtpos  6529  tfr0dm  6598  rdg0  6663  frec0g  6673  2oex  6709  1n0  6710  el1o  6715  0lt2o  6719  fnom  6728  omexg  6729  om0  6736  nnsucsssuc  6770  mapdm0  6942  map0e  6972  0elixp  7017  en0  7088  ensn1  7089  en1  7092  2dom  7099  map1  7107  rex2dom  7116  dom1o  7122  xp1en  7127  endisj  7128  dom0  7144  php5dom  7170  ssfilem  7183  ssfiexmid  7184  ssfilemd  7185  ssfiexmidt  7186  domfiexmid  7188  diffitest  7197  ac6sfi  7208  exmidpw  7221  exmidpw2en  7225  unfiexmid  7231  mapfi  7267  0fsupp  7305  fi0  7314  djuexb  7390  djulclr  7395  djulcl  7397  djulclb  7401  djulf1or  7402  djulf1o  7404  inl11  7411  djuss  7416  1stinl  7420  2ndinl  7421  0ct  7453  finomni  7486  exmidomni  7488  pr2cv1  7547  exmidonfinlem  7551  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  dju0en  7576  djucomen  7578  djuassen  7579  xpdjuen  7580  pw1dom2  7592  pw1ne1  7594  indpi  7715  frecfzennn  10883  fihashen1  11259  hashunlem  11265  hashmap  11289  hashfibc  11304  hashf1  11308  zfz1iso  11314  lswex  11377  s1prc  11412  ccat1st1st  11430  swrdval  11441  swrd0g  11453  pfxval  11467  pfx0g  11469  fnpfx  11470  swrdccat3blem  11532  fzf1o  12166  ennnfonelemj0  13349  ennnfonelem0  13353  ennnfonelemhom  13363  strsl0  13458  fnpr2ob  13719  xpsfrnel  13723  0g0  13754  gzsum0  13771  topgele  15272  en1top  15320  sn0topon  15331  sn0cld  15380  rest0  15422  restsn  15423  0met  15627  vtxval0  16516  iedgval0  16517  uhgr0  16548  upgr0eop  16585  usgr0  16702  usgr0eop  16705  griedg0prc  16713  0grsubgr  16727  clwwlk0on0  16894  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  djulclALT  17051  bj-charfun  17055  bj-d0clsepcl  17173  bj-indint  17179  bj-bdfindis  17195  bj-inf2vnlem1  17218  pw1map  17247  pwle2  17250  pw1nct  17255  wexmiddiffilem  17265  wexmiddifxylem  17267  idjudju  17269  0nninf  17270  nninfsellemdc  17276  nnnninfex  17288