Theorem 0ex 4221

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

Syntax hints:  ¬ wn 3  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2202  Vcvv 2803  ∅c0 3496

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-nul 4220

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-dif 3203  df-nul 3497

This theorem is referenced by:  0elpw  4260  0nep0  4261  iin0r  4265  intv  4266  snexprc  4282  p0ex  4284  undifexmid  4289  exmidexmid  4292  ss1o0el1  4293  exmidsssn  4298  exmidel  4301  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  0elon  4495  onm  4504  ordtriexmidlem2  4624  ordtriexmid  4625  ontriexmidim  4626  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  onsucelsucexmidlem1  4632  onsucelsucexmid  4634  regexmidlem1  4637  reg2exmidlema  4638  ordsoexmid  4666  0elsucexmid  4669  ordpwsucexmid  4674  ordtri2or2exmid  4675  ontri2orexmidim  4676  dcextest  4685  peano1  4698  finds  4704  finds2  4705  0elnn  4723  opthprc  4783  nfunv  5366  fun0  5395  acexmidlema  6019  acexmidlemb  6020  acexmidlemab  6022  ovprc  6064  1st0  6316  2nd0  6317  supp0  6416  fvn0elsupp  6429  fvn0elsuppb  6430  brtpos0  6461  reldmtpos  6462  tfr0dm  6531  rdg0  6596  frec0g  6606  2oex  6642  1n0  6643  el1o  6648  0lt2o  6652  fnom  6661  omexg  6662  om0  6669  nnsucsssuc  6703  mapdm0  6875  map0e  6898  0elixp  6941  en0  7012  ensn1  7013  en1  7016  2dom  7023  map1  7030  rex2dom  7039  dom1o  7045  xp1en  7050  endisj  7051  dom0  7067  php5dom  7092  ssfilem  7105  ssfiexmid  7106  ssfilemd  7107  ssfiexmidt  7108  domfiexmid  7110  diffitest  7119  ac6sfi  7130  exmidpw  7143  exmidpw2en  7147  unfiexmid  7153  fi0  7217  djuexb  7286  djulclr  7291  djulcl  7293  djulclb  7297  djulf1or  7298  djulf1o  7300  inl11  7307  djuss  7312  1stinl  7316  2ndinl  7317  0ct  7349  finomni  7382  exmidomni  7384  pr2cv1  7443  exmidonfinlem  7447  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidaclem  7466  dju0en  7472  djucomen  7474  djuassen  7475  xpdjuen  7476  pw1dom2  7488  pw1ne1  7490  indpi  7605  frecfzennn  10734  fihashen1  11107  hashunlem  11113  zfz1iso  11151  lswex  11214  s1prc  11249  ccat1st1st  11267  swrdval  11278  swrd0g  11290  pfxval  11304  pfx0g  11306  fnpfx  11307  swrdccat3blem  11369  fzf1o  11999  ennnfonelemj0  13085  ennnfonelem0  13089  ennnfonelemhom  13099  strsl0  13194  fnpr2ob  13486  xpsfrnel  13490  0g0  13522  gsum0g  13542  topgele  14823  en1top  14871  sn0topon  14882  sn0cld  14931  rest0  14973  restsn  14974  0met  15178  vtxval0  15977  iedgval0  15978  uhgr0  16009  upgr0eop  16046  usgr0  16163  usgr0eop  16166  griedg0prc  16174  0grsubgr  16188  clwwlk0on0  16355  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  djulclALT  16502  bj-charfun  16506  bj-d0clsepcl  16624  bj-indint  16630  bj-bdfindis  16646  bj-inf2vnlem1  16669  pw1map  16700  pwle2  16703  pw1nct  16708  0nninf  16713  nninfsellemdc  16719  nnnninfex  16731