Theorem 0ex 4130

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

Syntax hints:  ¬ wn 3  ∀wal 1351   = wceq 1353  ∃wex 1492   ∈ wcel 2148  Vcvv 2737  ∅c0 3422

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-nul 4129

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-dif 3131  df-nul 3423

This theorem is referenced by:  0elpw  4164  0nep0  4165  iin0r  4169  intv  4170  snexprc  4186  p0ex  4188  undifexmid  4193  exmidexmid  4196  ss1o0el1  4197  exmidsssn  4202  exmidel  4205  exmidundif  4206  exmidundifim  4207  exmid1stab  4208  0elon  4392  onm  4401  ordtriexmidlem2  4519  ordtriexmid  4520  ontriexmidim  4521  ordtri2orexmid  4522  ontr2exmid  4524  onsucsssucexmid  4526  onsucelsucexmidlem1  4527  onsucelsucexmid  4529  regexmidlem1  4532  reg2exmidlema  4533  ordsoexmid  4561  0elsucexmid  4564  ordpwsucexmid  4569  ordtri2or2exmid  4570  ontri2orexmidim  4571  dcextest  4580  peano1  4593  finds  4599  finds2  4600  0elnn  4618  opthprc  4677  nfunv  5249  fun0  5274  acexmidlema  5865  acexmidlemb  5866  acexmidlemab  5868  ovprc  5909  1st0  6144  2nd0  6145  brtpos0  6252  reldmtpos  6253  tfr0dm  6322  rdg0  6387  frec0g  6397  1n0  6432  el1o  6437  0lt2o  6441  fnom  6450  omexg  6451  om0  6458  nnsucsssuc  6492  mapdm0  6662  map0e  6685  0elixp  6728  en0  6794  ensn1  6795  en1  6798  2dom  6804  map1  6811  xp1en  6822  endisj  6823  dom0  6837  php5dom  6862  ssfilem  6874  ssfiexmid  6875  domfiexmid  6877  diffitest  6886  ac6sfi  6897  exmidpw  6907  unfiexmid  6916  fi0  6973  djuexb  7042  djulclr  7047  djulcl  7049  djulclb  7053  djulf1or  7054  djulf1o  7056  inl11  7063  djuss  7068  1stinl  7072  2ndinl  7073  0ct  7105  finomni  7137  exmidomni  7139  exmidonfinlem  7191  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  dju0en  7212  djucomen  7214  djuassen  7215  xpdjuen  7216  pw1dom2  7225  pw1ne1  7227  indpi  7340  frecfzennn  10425  fihashen1  10778  hashunlem  10783  zfz1iso  10820  ennnfonelemj0  12401  ennnfonelem0  12405  ennnfonelemhom  12415  strsl0  12510  fnpr2ob  12758  xpsfrnel  12762  0g0  12794  topgele  13499  en1top  13547  sn0topon  13558  sn0cld  13607  rest0  13649  restsn  13650  0met  13854  djulclALT  14523  fmelpw1o  14528  bj-charfun  14529  bj-d0clsepcl  14647  bj-indint  14653  bj-bdfindis  14669  bj-inf2vnlem1  14692  pwle2  14718  pw1nct  14722  0nninf  14723  nninfsellemdc  14729