Theorem 0ex 4210

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

Syntax hints:  ¬ wn 3  ∀wal 1393   = wceq 1395  ∃wex 1538   ∈ wcel 2200  Vcvv 2799  ∅c0 3491

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-nul 4209

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199  df-nul 3492

This theorem is referenced by:  0elpw  4247  0nep0  4248  iin0r  4252  intv  4253  snexprc  4269  p0ex  4271  undifexmid  4276  exmidexmid  4279  ss1o0el1  4280  exmidsssn  4285  exmidel  4288  exmidundif  4289  exmidundifim  4290  exmid1stab  4291  0elon  4482  onm  4491  ordtriexmidlem2  4611  ordtriexmid  4612  ontriexmidim  4613  ordtri2orexmid  4614  ontr2exmid  4616  onsucsssucexmid  4618  onsucelsucexmidlem1  4619  onsucelsucexmid  4621  regexmidlem1  4624  reg2exmidlema  4625  ordsoexmid  4653  0elsucexmid  4656  ordpwsucexmid  4661  ordtri2or2exmid  4662  ontri2orexmidim  4663  dcextest  4672  peano1  4685  finds  4691  finds2  4692  0elnn  4710  opthprc  4769  nfunv  5350  fun0  5378  acexmidlema  5991  acexmidlemb  5992  acexmidlemab  5994  ovprc  6036  1st0  6288  2nd0  6289  brtpos0  6396  reldmtpos  6397  tfr0dm  6466  rdg0  6531  frec0g  6541  1n0  6576  el1o  6581  0lt2o  6585  fnom  6594  omexg  6595  om0  6602  nnsucsssuc  6636  mapdm0  6808  map0e  6831  0elixp  6874  en0  6945  ensn1  6946  en1  6949  2dom  6956  map1  6963  rex2dom  6969  xp1en  6978  endisj  6979  dom0  6995  php5dom  7020  ssfilem  7033  ssfiexmid  7034  domfiexmid  7036  diffitest  7045  ac6sfi  7056  exmidpw  7066  exmidpw2en  7070  unfiexmid  7076  fi0  7138  djuexb  7207  djulclr  7212  djulcl  7214  djulclb  7218  djulf1or  7219  djulf1o  7221  inl11  7228  djuss  7233  1stinl  7237  2ndinl  7238  0ct  7270  finomni  7303  exmidomni  7305  pr2cv1  7364  exmidonfinlem  7367  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  exmidaclem  7386  dju0en  7392  djucomen  7394  djuassen  7395  xpdjuen  7396  pw1dom2  7408  pw1ne1  7410  fmelpw1o  7428  indpi  7525  frecfzennn  10643  fihashen1  11016  hashunlem  11021  zfz1iso  11058  lswex  11118  s1prc  11151  ccat1st1st  11167  swrdval  11175  swrd0g  11187  pfxval  11201  pfx0g  11203  fnpfx  11204  swrdccat3blem  11266  ennnfonelemj0  12967  ennnfonelem0  12971  ennnfonelemhom  12981  strsl0  13076  fnpr2ob  13368  xpsfrnel  13372  0g0  13404  gsum0g  13424  topgele  14697  en1top  14745  sn0topon  14756  sn0cld  14805  rest0  14847  restsn  14848  0met  15052  vtxval0  15848  iedgval0  15849  uhgr0  15879  upgr0eop  15916  djulclALT  16123  bj-charfun  16128  bj-d0clsepcl  16246  bj-indint  16252  bj-bdfindis  16268  bj-inf2vnlem1  16291  dom1o  16314  pw1map  16320  pwle2  16323  pw1nct  16328  0nninf  16329  nninfsellemdc  16335  nnnninfex  16347