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  6009  acexmidlemb  6010  acexmidlemab  6012  ovprc  6054  1st0  6307  2nd0  6308  brtpos0  6418  reldmtpos  6419  tfr0dm  6488  rdg0  6553  frec0g  6563  2oex  6599  1n0  6600  el1o  6605  0lt2o  6609  fnom  6618  omexg  6619  om0  6626  nnsucsssuc  6660  mapdm0  6832  map0e  6855  0elixp  6898  en0  6969  ensn1  6970  en1  6973  2dom  6980  map1  6987  rex2dom  6996  dom1o  7002  xp1en  7007  endisj  7008  dom0  7024  php5dom  7049  ssfilem  7062  ssfiexmid  7063  ssfilemd  7064  ssfiexmidt  7065  domfiexmid  7067  diffitest  7076  ac6sfi  7087  exmidpw  7100  exmidpw2en  7104  unfiexmid  7110  fi0  7174  djuexb  7243  djulclr  7248  djulcl  7250  djulclb  7254  djulf1or  7255  djulf1o  7257  inl11  7264  djuss  7269  1stinl  7273  2ndinl  7274  0ct  7306  finomni  7339  exmidomni  7341  pr2cv1  7400  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  dju0en  7429  djucomen  7431  djuassen  7432  xpdjuen  7433  pw1dom2  7445  pw1ne1  7447  fmelpw1o  7465  indpi  7562  frecfzennn  10689  fihashen1  11062  hashunlem  11068  zfz1iso  11106  lswex  11166  s1prc  11201  ccat1st1st  11219  swrdval  11230  swrd0g  11242  pfxval  11256  pfx0g  11258  fnpfx  11259  swrdccat3blem  11321  fzf1o  11938  ennnfonelemj0  13024  ennnfonelem0  13028  ennnfonelemhom  13038  strsl0  13133  fnpr2ob  13425  xpsfrnel  13429  0g0  13461  gsum0g  13481  topgele  14756  en1top  14804  sn0topon  14815  sn0cld  14864  rest0  14906  restsn  14907  0met  15111  vtxval0  15907  iedgval0  15908  uhgr0  15939  upgr0eop  15976  usgr0  16093  usgr0eop  16096  griedg0prc  16104  0grsubgr  16118  clwwlk0on0  16285  djulclALT  16414  bj-charfun  16419  bj-d0clsepcl  16537  bj-indint  16543  bj-bdfindis  16559  bj-inf2vnlem1  16582  pw1map  16613  pwle2  16616  pw1nct  16621  0nninf  16623  nninfsellemdc  16629  nnnninfex  16641