Theorem 0ex 4260

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209  Vcvv 2821  ∅c0 3520

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-nul 4259

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-dif 3222  df-nul 3521

This theorem is used by:  0elpw  4301  0nep0  4302  iin0r  4306  intv  4307  snexprc  4323  p0ex  4325  undifexmid  4330  exmidexmid  4333  ss1o0el1  4334  exmidsssn  4339  exmidel  4342  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  0elon  4537  onm  4546  ordtriexmidlem2  4667  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmidlem1  4675  onsucelsucexmid  4677  regexmidlem1  4680  reg2exmidlema  4681  ordsoexmid  4709  0elsucexmid  4712  ordpwsucexmid  4717  ordtri2or2exmid  4718  ontri2orexmidim  4719  dcextest  4728  peano1  4741  finds  4747  finds2  4748  0elnn  4766  opthprc  4826  nfunv  5410  fun0  5439  acexmidlema  6076  acexmidlemb  6077  acexmidlemab  6079  ovprc  6121  1st0  6378  2nd0  6379  supp0  6478  fvn0elsupp  6491  fvn0elsuppb  6492  brtpos0  6523  reldmtpos  6524  tfr0dm  6593  rdg0  6658  frec0g  6668  2oex  6704  1n0  6705  el1o  6710  0lt2o  6714  fnom  6723  omexg  6724  om0  6731  nnsucsssuc  6765  mapdm0  6937  map0e  6967  0elixp  7011  en0  7082  ensn1  7083  en1  7086  2dom  7093  map1  7101  rex2dom  7110  dom1o  7116  xp1en  7121  endisj  7122  dom0  7138  php5dom  7164  ssfilem  7177  ssfiexmid  7178  ssfilemd  7179  ssfiexmidt  7180  domfiexmid  7182  diffitest  7191  ac6sfi  7202  exmidpw  7215  exmidpw2en  7219  unfiexmid  7225  mapfi  7261  0fsupp  7298  fi0  7309  djuexb  7385  djulclr  7390  djulcl  7392  djulclb  7396  djulf1or  7397  djulf1o  7399  inl11  7406  djuss  7411  1stinl  7415  2ndinl  7416  0ct  7448  finomni  7481  exmidomni  7483  pr2cv1  7542  exmidonfinlem  7546  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  dju0en  7571  djucomen  7573  djuassen  7574  xpdjuen  7575  pw1dom2  7587  pw1ne1  7589  indpi  7710  frecfzennn  10878  fihashen1  11254  hashunlem  11260  hashmap  11284  hashfibc  11299  hashf1  11303  zfz1iso  11309  lswex  11372  s1prc  11407  ccat1st1st  11425  swrdval  11436  swrd0g  11448  pfxval  11462  pfx0g  11464  fnpfx  11465  swrdccat3blem  11527  fzf1o  12161  ennnfonelemj0  13344  ennnfonelem0  13348  ennnfonelemhom  13358  strsl0  13453  fnpr2ob  13714  xpsfrnel  13718  0g0  13749  gzsum0  13766  topgele  15221  en1top  15269  sn0topon  15280  sn0cld  15329  rest0  15371  restsn  15372  0met  15576  vtxval0  16460  iedgval0  16461  uhgr0  16492  upgr0eop  16529  usgr0  16646  usgr0eop  16649  griedg0prc  16657  0grsubgr  16671  clwwlk0on0  16838  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  djulclALT  16995  bj-charfun  16999  bj-d0clsepcl  17117  bj-indint  17123  bj-bdfindis  17139  bj-inf2vnlem1  17162  pw1map  17191  pwle2  17194  pw1nct  17199  wexmiddiffilem  17209  wexmiddifxylem  17211  0nninf  17213  nninfsellemdc  17219  nnnninfex  17231