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	⊢ ∅ ∈ V

Proof of Theorem 0ex

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-nul 4261	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 3540	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1658	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 146	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 2831	1 ⊢ ∅ ∈ V

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ 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  6527  reldmtpos  6528  tfr0dm  6597  rdg0  6662  frec0g  6672  2oex  6708  1n0  6709  el1o  6714  0lt2o  6718  fnom  6727  omexg  6728  om0  6735  nnsucsssuc  6769  mapdm0  6941  map0e  6971  0elixp  7015  en0  7086  ensn1  7087  en1  7090  2dom  7097  map1  7105  rex2dom  7114  dom1o  7120  xp1en  7125  endisj  7126  dom0  7142  php5dom  7168  ssfilem  7181  ssfiexmid  7182  ssfilemd  7183  ssfiexmidt  7184  domfiexmid  7186  diffitest  7195  ac6sfi  7206  exmidpw  7219  exmidpw2en  7223  unfiexmid  7229  mapfi  7265  0fsupp  7303  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  10884  fihashen1  11260  hashunlem  11266  hashmap  11290  hashfibc  11305  hashf1  11309  zfz1iso  11315  lswex  11378  s1prc  11413  ccat1st1st  11431  swrdval  11442  swrd0g  11454  pfxval  11468  pfx0g  11470  fnpfx  11471  swrdccat3blem  11533  fzf1o  12167  ennnfonelemj0  13350  ennnfonelem0  13354  ennnfonelemhom  13364  strsl0  13459  fnpr2ob  13720  xpsfrnel  13724  0g0  13755  gzsum0  13772  topgele  15255  en1top  15303  sn0topon  15314  sn0cld  15363  rest0  15405  restsn  15406  0met  15610  vtxval0  16499  iedgval0  16500  uhgr0  16531  upgr0eop  16568  usgr0  16685  usgr0eop  16688  griedg0prc  16696  0grsubgr  16710  clwwlk0on0  16877  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  djulclALT  17034  bj-charfun  17038  bj-d0clsepcl  17156  bj-indint  17162  bj-bdfindis  17178  bj-inf2vnlem1  17201  pw1map  17230  pwle2  17233  pw1nct  17238  wexmiddiffilem  17248  wexmiddifxylem  17250  idjudju  17252  0nninf  17253  nninfsellemdc  17259  nnnninfex  17271