Theorem 0ex 4050

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 4049. (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 4049	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 3376	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1584	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 145	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 2690	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1329   = wceq 1331  ∃wex 1468   ∈ wcel 1480  Vcvv 2681  ∅c0 3358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-nul 4049

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-dif 3068  df-nul 3359

This theorem is referenced by:  0elpw  4083  0nep0  4084  iin0r  4088  intv  4089  snexprc  4105  p0ex  4107  undifexmid  4112  exmidexmid  4115  exmid01  4116  exmidsssn  4120  exmidel  4123  exmidundif  4124  exmidundifim  4125  0elon  4309  onm  4318  ordtriexmidlem2  4431  ordtriexmid  4432  ordtri2orexmid  4433  ontr2exmid  4435  onsucsssucexmid  4437  onsucelsucexmidlem1  4438  onsucelsucexmid  4440  regexmidlem1  4443  reg2exmidlema  4444  ordsoexmid  4472  0elsucexmid  4475  ordpwsucexmid  4480  ordtri2or2exmid  4481  dcextest  4490  peano1  4503  finds  4509  finds2  4510  0elnn  4527  opthprc  4585  nfunv  5151  fun0  5176  acexmidlema  5758  acexmidlemb  5759  acexmidlemab  5761  ovprc  5799  1st0  6035  2nd0  6036  brtpos0  6142  reldmtpos  6143  tfr0dm  6212  rdg0  6277  frec0g  6287  1n0  6322  el1o  6327  0lt2o  6331  fnom  6339  omexg  6340  om0  6347  nnsucsssuc  6381  mapdm0  6550  map0e  6573  0elixp  6616  en0  6682  ensn1  6683  en1  6686  2dom  6692  map1  6699  xp1en  6710  endisj  6711  dom0  6725  php5dom  6750  ssfilem  6762  ssfiexmid  6763  domfiexmid  6765  diffitest  6774  ac6sfi  6785  exmidpw  6795  unfiexmid  6799  fi0  6856  djuexb  6922  djulclr  6927  djulcl  6929  djulclb  6933  djulf1or  6934  djulf1o  6936  inl11  6943  djuss  6948  1stinl  6952  2ndinl  6953  0ct  6985  finomni  7005  exmidomni  7007  exmidonfinlem  7042  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  dju0en  7063  djucomen  7065  djuassen  7066  xpdjuen  7067  indpi  7143  frecfzennn  10192  fihashen1  10538  hashunlem  10543  zfz1iso  10577  ennnfonelemj0  11903  ennnfonelem0  11907  ennnfonelemhom  11917  strsl0  11996  topgele  12185  en1top  12235  sn0topon  12246  sn0cld  12295  rest0  12337  restsn  12338  0met  12542  djulclALT  12997  bj-d0clsepcl  13112  bj-indint  13118  bj-bdfindis  13134  bj-inf2vnlem1  13157  pw1dom2  13179  pwle2  13182  exmid1stab  13184  0nninf  13186  nninfsellemdc  13195