Theorem 0fin 8916

Description: The empty set is finite. (Contributed by FL, 14-Jul-2008.)

Assertion

Ref	Expression
0fin	⊢ ∅ ∈ Fin

Proof of Theorem 0fin

Step	Hyp	Ref	Expression
1		peano1 7710	. 2 ⊢ ∅ ∈ ω
2		ssid 3939	. 2 ⊢ ∅ ⊆ ∅
3		ssnnfi 8914	. 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin)
4	1, 2, 3	mp2an 688	1 ⊢ ∅ ∈ Fin

Syntax hints:   ∈ wcel 2108   ⊆ wss 3883  ∅c0 4253  ωcom 7687  Fincfn 8691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-om 7688  df-en 8692  df-fin 8695

This theorem is referenced by:  ssfi  8918  imafi  8920  cnvfi  8924  fnfi  8925  nfielex  8976  xpfi  9015  iunfi  9037  fczfsuppd  9076  fsuppun  9077  0fsupp  9080  r1fin  9462  acndom  9738  numwdom  9746  ackbij1lem18  9924  sdom2en01  9989  fin23lem26  10012  isfin1-3  10073  gchxpidm  10356  fzfi  13620  fzofi  13622  hasheq0  14006  hashxp  14077  lcmf0  16267  0hashbc  16636  acsfn0  17286  isdrs2  17939  fpwipodrs  18173  symgfisg  18991  dsmm0cl  20857  mplsubg  21118  mpllss  21119  psrbag0  21180  mat0dimbas0  21523  mat0dim0  21524  mat0dimid  21525  mat0dimscm  21526  mat0dimcrng  21527  mat0scmat  21595  mavmul0  21609  mavmul0g  21610  mdet0pr  21649  m1detdiag  21654  d0mat2pmat  21795  chpmat0d  21891  fctop  22062  cmpfi  22467  bwth  22469  comppfsc  22591  ptbasid  22634  cfinfil  22952  ufinffr  22988  fin1aufil  22991  alexsubALTlem2  23107  alexsubALTlem4  23109  ptcmplem2  23112  tsmsfbas  23187  xrge0gsumle  23902  xrge0tsms  23903  fta1  25373  uhgr0edgfi  27510  fusgrfisbase  27598  vtxdg0e  27744  wwlksnfi  28172  hashxpe  31029  xrge0tsmsd  31219  esumnul  31916  esum0  31917  esumcst  31931  esumsnf  31932  esumpcvgval  31946  sibf0  32201  eulerpartlemt  32238  derang0  33031  topdifinffinlem  35445  matunitlindf  35702  0totbnd  35858  heiborlem6  35901  mzpcompact2lem  40489  rp-isfinite6  41023  0pwfi  42496  fouriercn  43663  rrxtopn0  43724  salexct  43763  sge0rnn0  43796  sge00  43804  sge0sn  43807  ovn0val  43978  ovn02  43996  hoidmv0val  44011  hoidmvle  44028  hoiqssbl  44053  von0val  44099  vonhoire  44100  vonioo  44110  vonicc  44113  vonsn  44119  lcoc0  45651  lco0  45656