Theorem 0ex 4258

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

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  4299  0nep0  4300  iin0r  4304  intv  4305  snexprc  4321  p0ex  4323  undifexmid  4328  exmidexmid  4331  ss1o0el1  4332  exmidsssn  4337  exmidel  4340  exmidundif  4341  exmidundifim  4342  exmid1stab  4343  0elon  4535  onm  4544  ordtriexmidlem2  4665  ordtriexmid  4666  ontriexmidim  4667  ordtri2orexmid  4668  ontr2exmid  4670  onsucsssucexmid  4672  onsucelsucexmidlem1  4673  onsucelsucexmid  4675  regexmidlem1  4678  reg2exmidlema  4679  ordsoexmid  4707  0elsucexmid  4710  ordpwsucexmid  4715  ordtri2or2exmid  4716  ontri2orexmidim  4717  dcextest  4726  peano1  4739  finds  4745  finds2  4746  0elnn  4764  opthprc  4824  nfunv  5408  fun0  5437  acexmidlema  6070  acexmidlemb  6071  acexmidlemab  6073  ovprc  6115  1st0  6372  2nd0  6373  supp0  6472  fvn0elsupp  6485  fvn0elsuppb  6486  brtpos0  6517  reldmtpos  6518  tfr0dm  6587  rdg0  6652  frec0g  6662  2oex  6698  1n0  6699  el1o  6704  0lt2o  6708  fnom  6717  omexg  6718  om0  6725  nnsucsssuc  6759  mapdm0  6931  map0e  6961  0elixp  7005  en0  7076  ensn1  7077  en1  7080  2dom  7087  map1  7095  rex2dom  7104  dom1o  7110  xp1en  7115  endisj  7116  dom0  7132  php5dom  7158  ssfilem  7171  ssfiexmid  7172  ssfilemd  7173  ssfiexmidt  7174  domfiexmid  7176  diffitest  7185  ac6sfi  7196  exmidpw  7209  exmidpw2en  7213  unfiexmid  7219  mapfi  7255  0fsupp  7292  fi0  7303  djuexb  7378  djulclr  7383  djulcl  7385  djulclb  7389  djulf1or  7390  djulf1o  7392  inl11  7399  djuss  7404  1stinl  7408  2ndinl  7409  0ct  7441  finomni  7474  exmidomni  7476  pr2cv1  7535  exmidonfinlem  7539  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  exmidaclem  7558  dju0en  7564  djucomen  7566  djuassen  7567  xpdjuen  7568  pw1dom2  7580  pw1ne1  7582  indpi  7703  frecfzennn  10846  fihashen1  11221  hashunlem  11227  hashmap  11251  hashfibc  11266  hashf1  11270  zfz1iso  11276  lswex  11339  s1prc  11374  ccat1st1st  11392  swrdval  11403  swrd0g  11415  pfxval  11429  pfx0g  11431  fnpfx  11432  swrdccat3blem  11494  fzf1o  12125  ennnfonelemj0  13275  ennnfonelem0  13279  ennnfonelemhom  13289  strsl0  13384  fnpr2ob  13644  xpsfrnel  13648  0g0  13679  gzsum0  13696  topgele  15113  en1top  15161  sn0topon  15172  sn0cld  15221  rest0  15263  restsn  15264  0met  15468  vtxval0  16277  iedgval0  16278  uhgr0  16309  upgr0eop  16346  usgr0  16463  usgr0eop  16466  griedg0prc  16474  0grsubgr  16488  clwwlk0on0  16655  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  djulclALT  16812  bj-charfun  16816  bj-d0clsepcl  16934  bj-indint  16940  bj-bdfindis  16956  bj-inf2vnlem1  16979  pw1map  17008  pwle2  17011  pw1nct  17016  0nninf  17022  nninfsellemdc  17028  nnnninfex  17040