Theorem 0fin 8458

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 7347	. 2 ⊢ ∅ ∈ ω
2		ssid 3849	. 2 ⊢ ∅ ⊆ ∅
3		ssnnfi 8449	. 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin)
4	1, 2, 3	mp2an 685	1 ⊢ ∅ ∈ Fin

Syntax hints:   ∈ wcel 2166   ⊆ wss 3799  ∅c0 4145  ωcom 7327  Fincfn 8223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-br 4875  df-opab 4937  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-om 7328  df-en 8224  df-fin 8227

This theorem is referenced by:  nfielex  8459  xpfi  8501  fnfi  8508  iunfi  8524  fczfsuppd  8563  fsuppun  8564  0fsupp  8567  r1fin  8914  acndom  9188  numwdom  9196  ackbij1lem18  9375  sdom2en01  9440  fin23lem26  9463  isfin1-3  9524  gchxpidm  9807  fzfi  13067  fzofi  13069  hasheq0  13445  hashxp  13511  lcmf0  15721  0hashbc  16083  acsfn0  16674  isdrs2  17293  fpwipodrs  17518  symgfisg  18239  mplsubg  19799  mpllss  19800  psrbag0  19855  dsmm0cl  20448  mat0dimbas0  20641  mat0dim0  20642  mat0dimid  20643  mat0dimscm  20644  mat0dimcrng  20645  mat0scmat  20713  mavmul0  20727  mavmul0g  20728  mdet0pr  20767  m1detdiag  20772  d0mat2pmat  20914  chpmat0d  21010  fctop  21180  cmpfi  21583  bwth  21585  comppfsc  21707  ptbasid  21750  cfinfil  22068  ufinffr  22104  fin1aufil  22107  alexsubALTlem2  22223  alexsubALTlem4  22225  ptcmplem2  22228  tsmsfbas  22302  xrge0gsumle  23007  xrge0tsms  23008  fta1  24463  uhgr0edgfi  26538  fusgrfisbase  26626  vtxdg0e  26773  wwlksnfi  27229  clwwlknfi  27391  xrge0tsmsd  30331  esumnul  30656  esum0  30657  esumcst  30671  esumsnf  30672  esumpcvgval  30686  sibf0  30942  eulerpartlemt  30979  derang0  31698  topdifinffinlem  33741  matunitlindf  33952  0totbnd  34115  heiborlem6  34158  mzpcompact2lem  38159  rp-isfinite6  38706  0pwfi  40045  fouriercn  41244  rrxtopn0  41305  salexct  41344  sge0rnn0  41377  sge00  41385  sge0sn  41388  ovn0val  41559  ovn02  41577  hoidmv0val  41592  hoidmvle  41609  hoiqssbl  41634  von0val  41680  vonhoire  41681  vonioo  41691  vonicc  41694  vonsn  41700  lcoc0  43059  lco0  43064