Theorem 0ex 4216

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 4215. (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 4215	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 3513	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1653	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 146	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 2812	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1395   = wceq 1397  ∃wex 1540   ∈ wcel 2202  Vcvv 2802  ∅c0 3494

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-nul 4215

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-dif 3202  df-nul 3495

This theorem is referenced by:  0elpw  4254  0nep0  4255  iin0r  4259  intv  4260  snexprc  4276  p0ex  4278  undifexmid  4283  exmidexmid  4286  ss1o0el1  4287  exmidsssn  4292  exmidel  4295  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  0elon  4489  onm  4498  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmidlem1  4626  onsucelsucexmid  4628  regexmidlem1  4631  reg2exmidlema  4632  ordsoexmid  4660  0elsucexmid  4663  ordpwsucexmid  4668  ordtri2or2exmid  4669  ontri2orexmidim  4670  dcextest  4679  peano1  4692  finds  4698  finds2  4699  0elnn  4717  opthprc  4777  nfunv  5359  fun0  5388  acexmidlema  6008  acexmidlemb  6009  acexmidlemab  6011  ovprc  6053  1st0  6306  2nd0  6307  brtpos0  6417  reldmtpos  6418  tfr0dm  6487  rdg0  6552  frec0g  6562  2oex  6598  1n0  6599  el1o  6604  0lt2o  6608  fnom  6617  omexg  6618  om0  6625  nnsucsssuc  6659  mapdm0  6831  map0e  6854  0elixp  6897  en0  6968  ensn1  6969  en1  6972  2dom  6979  map1  6986  rex2dom  6995  dom1o  7001  xp1en  7006  endisj  7007  dom0  7023  php5dom  7048  ssfilem  7061  ssfiexmid  7062  ssfilemd  7063  ssfiexmidt  7064  domfiexmid  7066  diffitest  7075  ac6sfi  7086  exmidpw  7099  exmidpw2en  7103  unfiexmid  7109  fi0  7173  djuexb  7242  djulclr  7247  djulcl  7249  djulclb  7253  djulf1or  7254  djulf1o  7256  inl11  7263  djuss  7268  1stinl  7272  2ndinl  7273  0ct  7305  finomni  7338  exmidomni  7340  pr2cv1  7399  exmidonfinlem  7403  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  dju0en  7428  djucomen  7430  djuassen  7431  xpdjuen  7432  pw1dom2  7444  pw1ne1  7446  fmelpw1o  7464  indpi  7561  frecfzennn  10687  fihashen1  11060  hashunlem  11066  zfz1iso  11104  lswex  11164  s1prc  11199  ccat1st1st  11217  swrdval  11228  swrd0g  11240  pfxval  11254  pfx0g  11256  fnpfx  11257  swrdccat3blem  11319  ennnfonelemj0  13021  ennnfonelem0  13025  ennnfonelemhom  13035  strsl0  13130  fnpr2ob  13422  xpsfrnel  13426  0g0  13458  gsum0g  13478  topgele  14752  en1top  14800  sn0topon  14811  sn0cld  14860  rest0  14902  restsn  14903  0met  15107  vtxval0  15903  iedgval0  15904  uhgr0  15935  upgr0eop  15972  usgr0  16089  usgr0eop  16092  griedg0prc  16100  0grsubgr  16114  clwwlk0on0  16281  djulclALT  16397  bj-charfun  16402  bj-d0clsepcl  16520  bj-indint  16526  bj-bdfindis  16542  bj-inf2vnlem1  16565  pw1map  16596  pwle2  16599  pw1nct  16604  0nninf  16606  nninfsellemdc  16612  nnnninfex  16624