Theorem 0ex 4255

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

Syntax hints:  ¬ wn 3  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209  Vcvv 2821  ∅c0 3520

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 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 4254

This theorem 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 referenced by:  0elpw  4296  0nep0  4297  iin0r  4301  intv  4302  snexprc  4318  p0ex  4320  undifexmid  4325  exmidexmid  4328  ss1o0el1  4329  exmidsssn  4334  exmidel  4337  exmidundif  4338  exmidundifim  4339  exmid1stab  4340  0elon  4532  onm  4541  ordtriexmidlem2  4662  ordtriexmid  4663  ontriexmidim  4664  ordtri2orexmid  4665  ontr2exmid  4667  onsucsssucexmid  4669  onsucelsucexmidlem1  4670  onsucelsucexmid  4672  regexmidlem1  4675  reg2exmidlema  4676  ordsoexmid  4704  0elsucexmid  4707  ordpwsucexmid  4712  ordtri2or2exmid  4713  ontri2orexmidim  4714  dcextest  4723  peano1  4736  finds  4742  finds2  4743  0elnn  4761  opthprc  4821  nfunv  5405  fun0  5434  acexmidlema  6066  acexmidlemb  6067  acexmidlemab  6069  ovprc  6111  1st0  6368  2nd0  6369  supp0  6468  fvn0elsupp  6481  fvn0elsuppb  6482  brtpos0  6513  reldmtpos  6514  tfr0dm  6583  rdg0  6648  frec0g  6658  2oex  6694  1n0  6695  el1o  6700  0lt2o  6704  fnom  6713  omexg  6714  om0  6721  nnsucsssuc  6755  mapdm0  6927  map0e  6957  0elixp  7001  en0  7072  ensn1  7073  en1  7076  2dom  7083  map1  7091  rex2dom  7100  dom1o  7106  xp1en  7111  endisj  7112  dom0  7128  php5dom  7154  ssfilem  7167  ssfiexmid  7168  ssfilemd  7169  ssfiexmidt  7170  domfiexmid  7172  diffitest  7181  ac6sfi  7192  exmidpw  7205  exmidpw2en  7209  unfiexmid  7215  mapfi  7251  0fsupp  7288  fi0  7299  djuexb  7374  djulclr  7379  djulcl  7381  djulclb  7385  djulf1or  7386  djulf1o  7388  inl11  7395  djuss  7400  1stinl  7404  2ndinl  7405  0ct  7437  finomni  7470  exmidomni  7472  pr2cv1  7531  exmidonfinlem  7535  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  dju0en  7560  djucomen  7562  djuassen  7563  xpdjuen  7564  pw1dom2  7576  pw1ne1  7578  indpi  7699  frecfzennn  10841  fihashen1  11216  hashunlem  11222  hashmap  11246  hashfibc  11261  hashf1  11265  zfz1iso  11271  lswex  11334  s1prc  11369  ccat1st1st  11387  swrdval  11398  swrd0g  11410  pfxval  11424  pfx0g  11426  fnpfx  11427  swrdccat3blem  11489  fzf1o  12120  ennnfonelemj0  13270  ennnfonelem0  13274  ennnfonelemhom  13284  strsl0  13379  fnpr2ob  13638  xpsfrnel  13642  0g0  13673  gzsum0  13690  topgele  15053  en1top  15101  sn0topon  15112  sn0cld  15161  rest0  15203  restsn  15204  0met  15408  vtxval0  16208  iedgval0  16209  uhgr0  16240  upgr0eop  16277  usgr0  16394  usgr0eop  16397  griedg0prc  16405  0grsubgr  16419  clwwlk0on0  16586  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  djulclALT  16743  bj-charfun  16747  bj-d0clsepcl  16865  bj-indint  16871  bj-bdfindis  16887  bj-inf2vnlem1  16910  pw1map  16939  pwle2  16942  pw1nct  16947  0nninf  16952  nninfsellemdc  16958  nnnninfex  16970