Theorem 0fin 9171

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 7879	. 2 ⊢ ∅ ∈ ω
2		ssid 4005	. 2 ⊢ ∅ ⊆ ∅
3		ssnnfi 9169	. 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin)
4	1, 2, 3	mp2an 691	1 ⊢ ∅ ∈ Fin

Syntax hints:   ∈ wcel 2107   ⊆ wss 3949  ∅c0 4323  ωcom 7855  Fincfn 8939

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-om 7856  df-en 8940  df-fin 8943

This theorem is referenced by:  ssfi  9173  imafi  9175  cnvfi  9180  fnfi  9181  nneneq  9209  nfielex  9273  xpfiOLD  9318  iunfi  9340  fczfsuppd  9381  fsuppun  9382  0fsupp  9385  r1fin  9768  acndom  10046  numwdom  10054  ackbij1lem18  10232  sdom2en01  10297  fin23lem26  10320  isfin1-3  10381  gchxpidm  10664  fzfi  13937  fzofi  13939  hasheq0  14323  hashxp  14394  lcmf0  16571  0hashbc  16940  acsfn0  17604  isdrs2  18259  fpwipodrs  18493  symgfisg  19336  dsmm0cl  21295  mplsubg  21561  mpllss  21562  psrbag0  21623  mat0dimbas0  21968  mat0dim0  21969  mat0dimid  21970  mat0dimscm  21971  mat0dimcrng  21972  mat0scmat  22040  mavmul0  22054  mavmul0g  22055  mdet0pr  22094  m1detdiag  22099  d0mat2pmat  22240  chpmat0d  22336  fctop  22507  cmpfi  22912  bwth  22914  comppfsc  23036  ptbasid  23079  cfinfil  23397  ufinffr  23433  fin1aufil  23436  alexsubALTlem2  23552  alexsubALTlem4  23554  ptcmplem2  23557  tsmsfbas  23632  xrge0gsumle  24349  xrge0tsms  24350  fta1  25821  uhgr0edgfi  28497  fusgrfisbase  28585  vtxdg0e  28731  wwlksnfi  29160  mptiffisupp  31915  hashxpe  32019  xrge0tsmsd  32209  esumnul  33046  esum0  33047  esumcst  33061  esumsnf  33062  esumpcvgval  33076  sibf0  33333  eulerpartlemt  33370  derang0  34160  topdifinffinlem  36228  matunitlindf  36486  0totbnd  36641  heiborlem6  36684  mzpcompact2lem  41489  rp-isfinite6  42269  0pwfi  43746  fouriercn  44948  rrxtopn0  45009  salexct  45050  sge0rnn0  45084  sge00  45092  sge0sn  45095  ovn0val  45266  ovn02  45284  hoidmv0val  45299  hoidmvle  45316  hoiqssbl  45341  von0val  45387  vonhoire  45388  vonioo  45398  vonicc  45401  vonsn  45407  lcoc0  47103  lco0  47108