Theorem 0ex 4214

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

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

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 4213

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 2802  df-dif 3200  df-nul 3493

This theorem is referenced by:  0elpw  4252  0nep0  4253  iin0r  4257  intv  4258  snexprc  4274  p0ex  4276  undifexmid  4281  exmidexmid  4284  ss1o0el1  4285  exmidsssn  4290  exmidel  4293  exmidundif  4294  exmidundifim  4295  exmid1stab  4296  0elon  4487  onm  4496  ordtriexmidlem2  4616  ordtriexmid  4617  ontriexmidim  4618  ordtri2orexmid  4619  ontr2exmid  4621  onsucsssucexmid  4623  onsucelsucexmidlem1  4624  onsucelsucexmid  4626  regexmidlem1  4629  reg2exmidlema  4630  ordsoexmid  4658  0elsucexmid  4661  ordpwsucexmid  4666  ordtri2or2exmid  4667  ontri2orexmidim  4668  dcextest  4677  peano1  4690  finds  4696  finds2  4697  0elnn  4715  opthprc  4775  nfunv  5357  fun0  5385  acexmidlema  6004  acexmidlemb  6005  acexmidlemab  6007  ovprc  6049  1st0  6302  2nd0  6303  brtpos0  6413  reldmtpos  6414  tfr0dm  6483  rdg0  6548  frec0g  6558  2oex  6594  1n0  6595  el1o  6600  0lt2o  6604  fnom  6613  omexg  6614  om0  6621  nnsucsssuc  6655  mapdm0  6827  map0e  6850  0elixp  6893  en0  6964  ensn1  6965  en1  6968  2dom  6975  map1  6982  rex2dom  6991  dom1o  6997  xp1en  7002  endisj  7003  dom0  7019  php5dom  7044  ssfilem  7057  ssfiexmid  7058  domfiexmid  7060  diffitest  7069  ac6sfi  7080  exmidpw  7093  exmidpw2en  7097  unfiexmid  7103  fi0  7165  djuexb  7234  djulclr  7239  djulcl  7241  djulclb  7245  djulf1or  7246  djulf1o  7248  inl11  7255  djuss  7260  1stinl  7264  2ndinl  7265  0ct  7297  finomni  7330  exmidomni  7332  pr2cv1  7391  exmidonfinlem  7394  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidaclem  7413  dju0en  7419  djucomen  7421  djuassen  7422  xpdjuen  7423  pw1dom2  7435  pw1ne1  7437  fmelpw1o  7455  indpi  7552  frecfzennn  10678  fihashen1  11051  hashunlem  11057  zfz1iso  11095  lswex  11155  s1prc  11190  ccat1st1st  11208  swrdval  11219  swrd0g  11231  pfxval  11245  pfx0g  11247  fnpfx  11248  swrdccat3blem  11310  ennnfonelemj0  13012  ennnfonelem0  13016  ennnfonelemhom  13026  strsl0  13121  fnpr2ob  13413  xpsfrnel  13417  0g0  13449  gsum0g  13469  topgele  14743  en1top  14791  sn0topon  14802  sn0cld  14851  rest0  14893  restsn  14894  0met  15098  vtxval0  15894  iedgval0  15895  uhgr0  15926  upgr0eop  15963  usgr0  16078  usgr0eop  16081  griedg0prc  16089  clwwlk0on0  16226  djulclALT  16333  bj-charfun  16338  bj-d0clsepcl  16456  bj-indint  16462  bj-bdfindis  16478  bj-inf2vnlem1  16501  pw1map  16532  pwle2  16535  pw1nct  16540  0nninf  16542  nninfsellemdc  16548  nnnninfex  16560