Theorem diffi 9101

Description: If 𝐴 is finite, (𝐴 ∖ 𝐵) is finite. (Contributed by FL, 3-Aug-2009.)

Assertion

Ref	Expression
diffi	⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin)

Proof of Theorem diffi

Step	Hyp	Ref	Expression
1		difss 4088	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssfi 9099	. 2 ⊢ ((𝐴 ∈ Fin ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴) → (𝐴 ∖ 𝐵) ∈ Fin)
3	1, 2	mpan2 691	1 ⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2113   ∖ cdif 3898   ⊆ wss 3901  Fincfn 8885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-om 7809  df-1o 8397  df-en 8886  df-fin 8889

This theorem is referenced by:  php  9133  dif1ennnALT  9179  fodomfir  9230  dif1card  9922  hashun2  14308  hashun3  14309  hashssdif  14337  hashdifpr  14340  hashfun  14362  hashf1lem2  14381  fsumsplit1  15670  fsumdifsnconst  15716  hash2iun1dif1  15749  incexc  15762  fprodeq0g  15919  fprodfvdvdsd  16263  ramub1lem1  16956  ramub1lem2  16957  prmdvdsprmo  16972  psgnprfval  19452  sylow2alem2  19549  sylow2a  19550  gsummgp0  20255  psgnfix1  21555  psgndiflemB  21557  psgndif  21559  copsgndif  21560  dmatmul  22443  submaval  22527  1marepvsma1  22529  gsummatr01lem3  22603  gsummatr01  22605  smadiadetlem3  22614  smadiadet  22616  cramerimplem1  22629  cmpcld  23348  alexsubALTlem3  23995  cldsubg  24057  xrge0gsumle  24780  amgm  26959  rpvmasum2  27481  numedglnl  29219  cusgrfilem3  29533  finsumvtxdg2ssteplem4  29624  finsumvtxdg2sstep  29625  diffib  32598  unidifsnel  32612  unidifsnne  32613  fprodeq02  32906  indsumin  32945  gsummptres  33137  cycpmconjslem2  33239  elrspunidl  33511  vietalem  33737  gsumesum  34218  ballotlemfp1  34651  ballotlemgun  34684  hgt750lemd  34807  hgt750lemb  34815  hgt750leme  34817  tgoldbachgtde  34819  subfacp1lem1  35375  subfacp1lem3  35378  topdifinfindis  37553  matunitlindflem1  37819  poimirlem25  37848  poimirlem26  37849  poimirlem27  37850  poimirlem30  37853  aks6d1c5lem3  42413  aks6d1c5lem2  42414  unitscyglem4  42474  elrfi  42957  eldioph2lem1  43023  eldioph2lem2  43024  pellexlem5  43096  fsumnncl  45839  fprod0  45863  dvmptfprodlem  46209  stoweidlem44  46309  stoweidlem57  46322  fourierdlem42  46414  fourierdlem102  46473  fourierdlem114  46485  etransclem25  46524  etransclem35  46534  hspmbllem2  46892  fsummsndifre  47639  fsummmodsndifre  47641  isubgr3stgrlem2  48234  mgpsumunsn  48628  mgpsumz  48629  mgpsumn  48630