Theorem 0fin 9122

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 7830	. 2 ⊢ ∅ ∈ ω
2		ssid 3969	. 2 ⊢ ∅ ⊆ ∅
3		ssnnfi 9120	. 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin)
4	1, 2, 3	mp2an 690	1 ⊢ ∅ ∈ Fin

Syntax hints:   ∈ wcel 2106   ⊆ wss 3913  ∅c0 4287  ωcom 7807  Fincfn 8890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-om 7808  df-en 8891  df-fin 8894

This theorem is referenced by:  ssfi  9124  imafi  9126  cnvfi  9131  fnfi  9132  nneneq  9160  nfielex  9224  xpfiOLD  9269  iunfi  9291  fczfsuppd  9332  fsuppun  9333  0fsupp  9336  r1fin  9718  acndom  9996  numwdom  10004  ackbij1lem18  10182  sdom2en01  10247  fin23lem26  10270  isfin1-3  10331  gchxpidm  10614  fzfi  13887  fzofi  13889  hasheq0  14273  hashxp  14344  lcmf0  16521  0hashbc  16890  acsfn0  17554  isdrs2  18209  fpwipodrs  18443  symgfisg  19264  dsmm0cl  21183  mplsubg  21445  mpllss  21446  psrbag0  21507  mat0dimbas0  21852  mat0dim0  21853  mat0dimid  21854  mat0dimscm  21855  mat0dimcrng  21856  mat0scmat  21924  mavmul0  21938  mavmul0g  21939  mdet0pr  21978  m1detdiag  21983  d0mat2pmat  22124  chpmat0d  22220  fctop  22391  cmpfi  22796  bwth  22798  comppfsc  22920  ptbasid  22963  cfinfil  23281  ufinffr  23317  fin1aufil  23320  alexsubALTlem2  23436  alexsubALTlem4  23438  ptcmplem2  23441  tsmsfbas  23516  xrge0gsumle  24233  xrge0tsms  24234  fta1  25705  uhgr0edgfi  28251  fusgrfisbase  28339  vtxdg0e  28485  wwlksnfi  28914  mptiffisupp  31675  hashxpe  31779  xrge0tsmsd  31969  esumnul  32736  esum0  32737  esumcst  32751  esumsnf  32752  esumpcvgval  32766  sibf0  33023  eulerpartlemt  33060  derang0  33850  topdifinffinlem  35891  matunitlindf  36149  0totbnd  36305  heiborlem6  36348  mzpcompact2lem  41132  rp-isfinite6  41912  0pwfi  43389  fouriercn  44593  rrxtopn0  44654  salexct  44695  sge0rnn0  44729  sge00  44737  sge0sn  44740  ovn0val  44911  ovn02  44929  hoidmv0val  44944  hoidmvle  44961  hoiqssbl  44986  von0val  45032  vonhoire  45033  vonioo  45043  vonicc  45046  vonsn  45052  lcoc0  46623  lco0  46628