Theorem 0ex 4178

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

Syntax hints:  ¬ wn 3  ∀wal 1371   = wceq 1373  ∃wex 1516   ∈ wcel 2177  Vcvv 2773  ∅c0 3464

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-nul 4177

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-dif 3172  df-nul 3465

This theorem is referenced by:  0elpw  4215  0nep0  4216  iin0r  4220  intv  4221  snexprc  4237  p0ex  4239  undifexmid  4244  exmidexmid  4247  ss1o0el1  4248  exmidsssn  4253  exmidel  4256  exmidundif  4257  exmidundifim  4258  exmid1stab  4259  0elon  4446  onm  4455  ordtriexmidlem2  4575  ordtriexmid  4576  ontriexmidim  4577  ordtri2orexmid  4578  ontr2exmid  4580  onsucsssucexmid  4582  onsucelsucexmidlem1  4583  onsucelsucexmid  4585  regexmidlem1  4588  reg2exmidlema  4589  ordsoexmid  4617  0elsucexmid  4620  ordpwsucexmid  4625  ordtri2or2exmid  4626  ontri2orexmidim  4627  dcextest  4636  peano1  4649  finds  4655  finds2  4656  0elnn  4674  opthprc  4733  nfunv  5312  fun0  5340  acexmidlema  5947  acexmidlemb  5948  acexmidlemab  5950  ovprc  5992  1st0  6242  2nd0  6243  brtpos0  6350  reldmtpos  6351  tfr0dm  6420  rdg0  6485  frec0g  6495  1n0  6530  el1o  6535  0lt2o  6539  fnom  6548  omexg  6549  om0  6556  nnsucsssuc  6590  mapdm0  6762  map0e  6785  0elixp  6828  en0  6899  ensn1  6900  en1  6903  2dom  6910  map1  6917  rex2dom  6923  xp1en  6932  endisj  6933  dom0  6949  php5dom  6974  ssfilem  6986  ssfiexmid  6987  domfiexmid  6989  diffitest  6998  ac6sfi  7009  exmidpw  7019  exmidpw2en  7023  unfiexmid  7029  fi0  7091  djuexb  7160  djulclr  7165  djulcl  7167  djulclb  7171  djulf1or  7172  djulf1o  7174  inl11  7181  djuss  7186  1stinl  7190  2ndinl  7191  0ct  7223  finomni  7256  exmidomni  7258  exmidonfinlem  7316  exmidfodomrlemr  7325  exmidfodomrlemrALT  7326  exmidaclem  7335  dju0en  7341  djucomen  7343  djuassen  7344  xpdjuen  7345  pw1dom2  7354  pw1ne1  7356  indpi  7470  frecfzennn  10588  fihashen1  10961  hashunlem  10966  zfz1iso  11003  lswex  11062  s1prc  11095  ccat1st1st  11111  swrdval  11119  swrd0g  11131  pfxval  11145  pfx0g  11147  fnpfx  11148  ennnfonelemj0  12842  ennnfonelem0  12846  ennnfonelemhom  12856  strsl0  12951  fnpr2ob  13242  xpsfrnel  13246  0g0  13278  gsum0g  13298  topgele  14571  en1top  14619  sn0topon  14630  sn0cld  14679  rest0  14721  restsn  14722  0met  14926  vtxval0  15720  iedgval0  15721  uhgr0  15751  upgr0eop  15785  djulclALT  15871  fmelpw1o  15876  bj-charfun  15877  bj-d0clsepcl  15995  bj-indint  16001  bj-bdfindis  16017  bj-inf2vnlem1  16040  dom1o  16063  pwle2  16070  pw1nct  16075  0nninf  16076  nninfsellemdc  16082  nnnninfex  16094