Theorem 0ex 4161

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

Syntax hints:  ¬ wn 3  ∀wal 1362   = wceq 1364  ∃wex 1506   ∈ wcel 2167  Vcvv 2763  ∅c0 3451

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-nul 4160

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-dif 3159  df-nul 3452

This theorem is referenced by:  0elpw  4198  0nep0  4199  iin0r  4203  intv  4204  snexprc  4220  p0ex  4222  undifexmid  4227  exmidexmid  4230  ss1o0el1  4231  exmidsssn  4236  exmidel  4239  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  0elon  4428  onm  4437  ordtriexmidlem2  4557  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  ontr2exmid  4562  onsucsssucexmid  4564  onsucelsucexmidlem1  4565  onsucelsucexmid  4567  regexmidlem1  4570  reg2exmidlema  4571  ordsoexmid  4599  0elsucexmid  4602  ordpwsucexmid  4607  ordtri2or2exmid  4608  ontri2orexmidim  4609  dcextest  4618  peano1  4631  finds  4637  finds2  4638  0elnn  4656  opthprc  4715  nfunv  5292  fun0  5317  acexmidlema  5916  acexmidlemb  5917  acexmidlemab  5919  ovprc  5961  1st0  6211  2nd0  6212  brtpos0  6319  reldmtpos  6320  tfr0dm  6389  rdg0  6454  frec0g  6464  1n0  6499  el1o  6504  0lt2o  6508  fnom  6517  omexg  6518  om0  6525  nnsucsssuc  6559  mapdm0  6731  map0e  6754  0elixp  6797  en0  6863  ensn1  6864  en1  6867  2dom  6873  map1  6880  xp1en  6891  endisj  6892  dom0  6908  php5dom  6933  ssfilem  6945  ssfiexmid  6946  domfiexmid  6948  diffitest  6957  ac6sfi  6968  exmidpw  6978  exmidpw2en  6982  unfiexmid  6988  fi0  7050  djuexb  7119  djulclr  7124  djulcl  7126  djulclb  7130  djulf1or  7131  djulf1o  7133  inl11  7140  djuss  7145  1stinl  7149  2ndinl  7150  0ct  7182  finomni  7215  exmidomni  7217  exmidonfinlem  7272  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  exmidaclem  7291  dju0en  7297  djucomen  7299  djuassen  7300  xpdjuen  7301  pw1dom2  7310  pw1ne1  7312  indpi  7426  frecfzennn  10535  fihashen1  10908  hashunlem  10913  zfz1iso  10950  ennnfonelemj0  12643  ennnfonelem0  12647  ennnfonelemhom  12657  strsl0  12752  fnpr2ob  13042  xpsfrnel  13046  0g0  13078  gsum0g  13098  topgele  14349  en1top  14397  sn0topon  14408  sn0cld  14457  rest0  14499  restsn  14500  0met  14704  djulclALT  15531  fmelpw1o  15536  bj-charfun  15537  bj-d0clsepcl  15655  bj-indint  15661  bj-bdfindis  15677  bj-inf2vnlem1  15700  pwle2  15729  pw1nct  15734  0nninf  15735  nninfsellemdc  15741