Theorem 0ex 4109

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

Syntax hints:  ¬ wn 3  ∀wal 1341   = wceq 1343  ∃wex 1480   ∈ wcel 2136  Vcvv 2726  ∅c0 3409

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 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-nul 4108

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-dif 3118  df-nul 3410

This theorem is referenced by:  0elpw  4143  0nep0  4144  iin0r  4148  intv  4149  snexprc  4165  p0ex  4167  undifexmid  4172  exmidexmid  4175  ss1o0el1  4176  exmidsssn  4181  exmidel  4184  exmidundif  4185  exmidundifim  4186  0elon  4370  onm  4379  ordtriexmidlem2  4497  ordtriexmid  4498  ontriexmidim  4499  ordtri2orexmid  4500  ontr2exmid  4502  onsucsssucexmid  4504  onsucelsucexmidlem1  4505  onsucelsucexmid  4507  regexmidlem1  4510  reg2exmidlema  4511  ordsoexmid  4539  0elsucexmid  4542  ordpwsucexmid  4547  ordtri2or2exmid  4548  ontri2orexmidim  4549  dcextest  4558  peano1  4571  finds  4577  finds2  4578  0elnn  4596  opthprc  4655  nfunv  5221  fun0  5246  acexmidlema  5833  acexmidlemb  5834  acexmidlemab  5836  ovprc  5877  1st0  6112  2nd0  6113  brtpos0  6220  reldmtpos  6221  tfr0dm  6290  rdg0  6355  frec0g  6365  1n0  6400  el1o  6405  0lt2o  6409  fnom  6418  omexg  6419  om0  6426  nnsucsssuc  6460  mapdm0  6629  map0e  6652  0elixp  6695  en0  6761  ensn1  6762  en1  6765  2dom  6771  map1  6778  xp1en  6789  endisj  6790  dom0  6804  php5dom  6829  ssfilem  6841  ssfiexmid  6842  domfiexmid  6844  diffitest  6853  ac6sfi  6864  exmidpw  6874  unfiexmid  6883  fi0  6940  djuexb  7009  djulclr  7014  djulcl  7016  djulclb  7020  djulf1or  7021  djulf1o  7023  inl11  7030  djuss  7035  1stinl  7039  2ndinl  7040  0ct  7072  finomni  7104  exmidomni  7106  exmidonfinlem  7149  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  dju0en  7170  djucomen  7172  djuassen  7173  xpdjuen  7174  pw1dom2  7183  pw1ne1  7185  indpi  7283  frecfzennn  10361  fihashen1  10712  hashunlem  10717  zfz1iso  10754  ennnfonelemj0  12334  ennnfonelem0  12338  ennnfonelemhom  12348  strsl0  12442  0g0  12607  topgele  12667  en1top  12717  sn0topon  12728  sn0cld  12777  rest0  12819  restsn  12820  0met  13024  djulclALT  13682  fmelpw1o  13688  bj-charfun  13689  bj-d0clsepcl  13807  bj-indint  13813  bj-bdfindis  13829  bj-inf2vnlem1  13852  pwle2  13878  exmid1stab  13880  pw1nct  13883  0nninf  13884  nninfsellemdc  13890