Theorem 0ex 3995

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

Syntax hints:  ¬ wn 3  ∀wal 1297   = wceq 1299  ∃wex 1436   ∈ wcel 1448  Vcvv 2641  ∅c0 3310

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-nul 3994

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-dif 3023  df-nul 3311

This theorem is referenced by:  0elpw  4028  0nep0  4029  iin0r  4033  intv  4034  snexprc  4050  p0ex  4052  undifexmid  4057  exmidexmid  4060  exmid01  4061  exmidsssn  4063  exmidel  4066  exmidundif  4067  exmidundifim  4068  0elon  4252  onm  4261  ordtriexmidlem2  4374  ordtriexmid  4375  ordtri2orexmid  4376  ontr2exmid  4378  onsucsssucexmid  4380  onsucelsucexmidlem1  4381  onsucelsucexmid  4383  regexmidlem1  4386  reg2exmidlema  4387  ordsoexmid  4415  0elsucexmid  4418  ordpwsucexmid  4423  ordtri2or2exmid  4424  dcextest  4433  peano1  4446  finds  4452  finds2  4453  0elnn  4470  opthprc  4528  nfunv  5092  fun0  5117  acexmidlema  5697  acexmidlemb  5698  acexmidlemab  5700  ovprc  5738  1st0  5973  2nd0  5974  brtpos0  6079  reldmtpos  6080  tfr0dm  6149  rdg0  6214  frec0g  6224  1n0  6259  el1o  6264  0lt2o  6268  fnom  6276  omexg  6277  om0  6284  nnsucsssuc  6318  mapdm0  6487  map0e  6510  0elixp  6553  en0  6619  ensn1  6620  en1  6623  2dom  6629  map1  6636  xp1en  6646  endisj  6647  dom0  6661  php5dom  6686  ssfilem  6698  ssfiexmid  6699  domfiexmid  6701  diffitest  6710  ac6sfi  6721  exmidpw  6731  unfiexmid  6735  djuexb  6844  djulclr  6849  djulcl  6851  djulclb  6855  djulf1or  6856  djulf1o  6858  inl11  6865  djuss  6870  1stinl  6874  2ndinl  6875  0ct  6907  finomni  6924  exmidomni  6926  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  dju0en  6974  djucomen  6976  djuassen  6977  xpdjuen  6978  indpi  7051  frecfzennn  10040  fihashen1  10386  hashunlem  10391  zfz1iso  10425  ennnfonelemj0  11706  ennnfonelem0  11710  ennnfonelemhom  11720  strsl0  11789  topgele  11978  en1top  12028  sn0topon  12039  sn0cld  12088  rest0  12130  restsn  12131  0met  12312  djulclALT  12589  bj-d0clsepcl  12708  bj-indint  12714  bj-bdfindis  12730  bj-inf2vnlem1  12753  pw1dom2  12775  pwle2  12779  0nninf  12781  nninfsellemdc  12790