Theorem 0ex 4156

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

Syntax hints:  ¬ wn 3  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2164  Vcvv 2760  ∅c0 3446

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-nul 4155

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-dif 3155  df-nul 3447

This theorem is referenced by:  0elpw  4193  0nep0  4194  iin0r  4198  intv  4199  snexprc  4215  p0ex  4217  undifexmid  4222  exmidexmid  4225  ss1o0el1  4226  exmidsssn  4231  exmidel  4234  exmidundif  4235  exmidundifim  4236  exmid1stab  4237  0elon  4423  onm  4432  ordtriexmidlem2  4552  ordtriexmid  4553  ontriexmidim  4554  ordtri2orexmid  4555  ontr2exmid  4557  onsucsssucexmid  4559  onsucelsucexmidlem1  4560  onsucelsucexmid  4562  regexmidlem1  4565  reg2exmidlema  4566  ordsoexmid  4594  0elsucexmid  4597  ordpwsucexmid  4602  ordtri2or2exmid  4603  ontri2orexmidim  4604  dcextest  4613  peano1  4626  finds  4632  finds2  4633  0elnn  4651  opthprc  4710  nfunv  5287  fun0  5312  acexmidlema  5909  acexmidlemb  5910  acexmidlemab  5912  ovprc  5953  1st0  6197  2nd0  6198  brtpos0  6305  reldmtpos  6306  tfr0dm  6375  rdg0  6440  frec0g  6450  1n0  6485  el1o  6490  0lt2o  6494  fnom  6503  omexg  6504  om0  6511  nnsucsssuc  6545  mapdm0  6717  map0e  6740  0elixp  6783  en0  6849  ensn1  6850  en1  6853  2dom  6859  map1  6866  xp1en  6877  endisj  6878  dom0  6894  php5dom  6919  ssfilem  6931  ssfiexmid  6932  domfiexmid  6934  diffitest  6943  ac6sfi  6954  exmidpw  6964  exmidpw2en  6968  unfiexmid  6974  fi0  7034  djuexb  7103  djulclr  7108  djulcl  7110  djulclb  7114  djulf1or  7115  djulf1o  7117  inl11  7124  djuss  7129  1stinl  7133  2ndinl  7134  0ct  7166  finomni  7199  exmidomni  7201  exmidonfinlem  7253  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  dju0en  7274  djucomen  7276  djuassen  7277  xpdjuen  7278  pw1dom2  7287  pw1ne1  7289  indpi  7402  frecfzennn  10497  fihashen1  10870  hashunlem  10875  zfz1iso  10912  ennnfonelemj0  12558  ennnfonelem0  12562  ennnfonelemhom  12572  strsl0  12667  fnpr2ob  12923  xpsfrnel  12927  0g0  12959  gsum0g  12979  topgele  14197  en1top  14245  sn0topon  14256  sn0cld  14305  rest0  14347  restsn  14348  0met  14552  djulclALT  15293  fmelpw1o  15298  bj-charfun  15299  bj-d0clsepcl  15417  bj-indint  15423  bj-bdfindis  15439  bj-inf2vnlem1  15462  pwle2  15489  pw1nct  15493  0nninf  15494  nninfsellemdc  15500