Theorem 0ex 4116

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

Syntax hints:  ¬ wn 3  ∀wal 1346   = wceq 1348  ∃wex 1485   ∈ wcel 2141  Vcvv 2730  ∅c0 3414

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-nul 4115

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123  df-nul 3415

This theorem is referenced by:  0elpw  4150  0nep0  4151  iin0r  4155  intv  4156  snexprc  4172  p0ex  4174  undifexmid  4179  exmidexmid  4182  ss1o0el1  4183  exmidsssn  4188  exmidel  4191  exmidundif  4192  exmidundifim  4193  0elon  4377  onm  4386  ordtriexmidlem2  4504  ordtriexmid  4505  ontriexmidim  4506  ordtri2orexmid  4507  ontr2exmid  4509  onsucsssucexmid  4511  onsucelsucexmidlem1  4512  onsucelsucexmid  4514  regexmidlem1  4517  reg2exmidlema  4518  ordsoexmid  4546  0elsucexmid  4549  ordpwsucexmid  4554  ordtri2or2exmid  4555  ontri2orexmidim  4556  dcextest  4565  peano1  4578  finds  4584  finds2  4585  0elnn  4603  opthprc  4662  nfunv  5231  fun0  5256  acexmidlema  5844  acexmidlemb  5845  acexmidlemab  5847  ovprc  5888  1st0  6123  2nd0  6124  brtpos0  6231  reldmtpos  6232  tfr0dm  6301  rdg0  6366  frec0g  6376  1n0  6411  el1o  6416  0lt2o  6420  fnom  6429  omexg  6430  om0  6437  nnsucsssuc  6471  mapdm0  6641  map0e  6664  0elixp  6707  en0  6773  ensn1  6774  en1  6777  2dom  6783  map1  6790  xp1en  6801  endisj  6802  dom0  6816  php5dom  6841  ssfilem  6853  ssfiexmid  6854  domfiexmid  6856  diffitest  6865  ac6sfi  6876  exmidpw  6886  unfiexmid  6895  fi0  6952  djuexb  7021  djulclr  7026  djulcl  7028  djulclb  7032  djulf1or  7033  djulf1o  7035  inl11  7042  djuss  7047  1stinl  7051  2ndinl  7052  0ct  7084  finomni  7116  exmidomni  7118  exmidonfinlem  7170  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  dju0en  7191  djucomen  7193  djuassen  7194  xpdjuen  7195  pw1dom2  7204  pw1ne1  7206  indpi  7304  frecfzennn  10382  fihashen1  10734  hashunlem  10739  zfz1iso  10776  ennnfonelemj0  12356  ennnfonelem0  12360  ennnfonelemhom  12370  strsl0  12464  0g0  12630  topgele  12821  en1top  12871  sn0topon  12882  sn0cld  12931  rest0  12973  restsn  12974  0met  13178  djulclALT  13836  fmelpw1o  13841  bj-charfun  13842  bj-d0clsepcl  13960  bj-indint  13966  bj-bdfindis  13982  bj-inf2vnlem1  14005  pwle2  14031  exmid1stab  14033  pw1nct  14036  0nninf  14037  nninfsellemdc  14043