Theorem 0fin 8954

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 7735	. 2 ⊢ ∅ ∈ ω
2		ssid 3943	. 2 ⊢ ∅ ⊆ ∅
3		ssnnfi 8952	. 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin)
4	1, 2, 3	mp2an 689	1 ⊢ ∅ ∈ Fin

Syntax hints:   ∈ wcel 2106   ⊆ wss 3887  ∅c0 4256  ωcom 7712  Fincfn 8733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-om 7713  df-en 8734  df-fin 8737

This theorem is referenced by:  ssfi  8956  imafi  8958  cnvfi  8963  fnfi  8964  nneneq  8992  nfielex  9047  xpfi  9085  iunfi  9107  fczfsuppd  9146  fsuppun  9147  0fsupp  9150  r1fin  9531  acndom  9807  numwdom  9815  ackbij1lem18  9993  sdom2en01  10058  fin23lem26  10081  isfin1-3  10142  gchxpidm  10425  fzfi  13692  fzofi  13694  hasheq0  14078  hashxp  14149  lcmf0  16339  0hashbc  16708  acsfn0  17369  isdrs2  18024  fpwipodrs  18258  symgfisg  19076  dsmm0cl  20947  mplsubg  21208  mpllss  21209  psrbag0  21270  mat0dimbas0  21615  mat0dim0  21616  mat0dimid  21617  mat0dimscm  21618  mat0dimcrng  21619  mat0scmat  21687  mavmul0  21701  mavmul0g  21702  mdet0pr  21741  m1detdiag  21746  d0mat2pmat  21887  chpmat0d  21983  fctop  22154  cmpfi  22559  bwth  22561  comppfsc  22683  ptbasid  22726  cfinfil  23044  ufinffr  23080  fin1aufil  23083  alexsubALTlem2  23199  alexsubALTlem4  23201  ptcmplem2  23204  tsmsfbas  23279  xrge0gsumle  23996  xrge0tsms  23997  fta1  25468  uhgr0edgfi  27607  fusgrfisbase  27695  vtxdg0e  27841  wwlksnfi  28271  hashxpe  31127  xrge0tsmsd  31317  esumnul  32016  esum0  32017  esumcst  32031  esumsnf  32032  esumpcvgval  32046  sibf0  32301  eulerpartlemt  32338  derang0  33131  topdifinffinlem  35518  matunitlindf  35775  0totbnd  35931  heiborlem6  35974  mzpcompact2lem  40573  rp-isfinite6  41125  0pwfi  42607  fouriercn  43773  rrxtopn0  43834  salexct  43873  sge0rnn0  43906  sge00  43914  sge0sn  43917  ovn0val  44088  ovn02  44106  hoidmv0val  44121  hoidmvle  44138  hoiqssbl  44163  von0val  44209  vonhoire  44210  vonioo  44220  vonicc  44223  vonsn  44229  lcoc0  45763  lco0  45768