Theorem 0ex 4260

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 4259. (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 4259	. . 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 4259

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  4301  0nep0  4302  iin0r  4306  intv  4307  snexprc  4323  p0ex  4325  undifexmid  4330  exmidexmid  4333  ss1o0el1  4334  exmidsssn  4339  exmidel  4342  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  0elon  4537  onm  4546  ordtriexmidlem2  4667  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmidlem1  4675  onsucelsucexmid  4677  regexmidlem1  4680  reg2exmidlema  4681  ordsoexmid  4709  0elsucexmid  4712  ordpwsucexmid  4717  ordtri2or2exmid  4718  ontri2orexmidim  4719  dcextest  4728  peano1  4741  finds  4747  finds2  4748  0elnn  4766  opthprc  4826  nfunv  5410  fun0  5439  acexmidlema  6076  acexmidlemb  6077  acexmidlemab  6079  ovprc  6121  1st0  6378  2nd0  6379  supp0  6478  fvn0elsupp  6491  fvn0elsuppb  6492  brtpos0  6523  reldmtpos  6524  tfr0dm  6593  rdg0  6658  frec0g  6668  2oex  6704  1n0  6705  el1o  6710  0lt2o  6714  fnom  6723  omexg  6724  om0  6731  nnsucsssuc  6765  mapdm0  6937  map0e  6967  0elixp  7011  en0  7082  ensn1  7083  en1  7086  2dom  7093  map1  7101  rex2dom  7110  dom1o  7116  xp1en  7121  endisj  7122  dom0  7138  php5dom  7164  ssfilem  7177  ssfiexmid  7178  ssfilemd  7179  ssfiexmidt  7180  domfiexmid  7182  diffitest  7191  ac6sfi  7202  exmidpw  7215  exmidpw2en  7219  unfiexmid  7225  mapfi  7261  0fsupp  7298  fi0  7309  djuexb  7384  djulclr  7389  djulcl  7391  djulclb  7395  djulf1or  7396  djulf1o  7398  inl11  7405  djuss  7410  1stinl  7414  2ndinl  7415  0ct  7447  finomni  7480  exmidomni  7482  pr2cv1  7541  exmidonfinlem  7545  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  dju0en  7570  djucomen  7572  djuassen  7573  xpdjuen  7574  pw1dom2  7586  pw1ne1  7588  indpi  7709  frecfzennn  10863  fihashen1  11238  hashunlem  11244  hashmap  11268  hashfibc  11283  hashf1  11287  zfz1iso  11293  lswex  11356  s1prc  11391  ccat1st1st  11409  swrdval  11420  swrd0g  11432  pfxval  11446  pfx0g  11448  fnpfx  11449  swrdccat3blem  11511  fzf1o  12142  ennnfonelemj0  13292  ennnfonelem0  13296  ennnfonelemhom  13306  strsl0  13401  fnpr2ob  13661  xpsfrnel  13665  0g0  13696  gzsum0  13713  topgele  15130  en1top  15178  sn0topon  15189  sn0cld  15238  rest0  15280  restsn  15281  0met  15485  vtxval0  16294  iedgval0  16295  uhgr0  16326  upgr0eop  16363  usgr0  16480  usgr0eop  16483  griedg0prc  16491  0grsubgr  16505  clwwlk0on0  16672  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  djulclALT  16829  bj-charfun  16833  bj-d0clsepcl  16951  bj-indint  16957  bj-bdfindis  16973  bj-inf2vnlem1  16996  pw1map  17025  pwle2  17028  pw1nct  17033  wexmiddiffilem  17043  wexmiddifxylem  17045  0nninf  17047  nninfsellemdc  17053  nnnninfex  17065