Theorem diffi 9109

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 4076	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2		ssfi 9107	. 2 ⊢ ((𝐴 ∈ Fin ∧ (𝐴 ∖ 𝐵) ⊆ 𝐴) → (𝐴 ∖ 𝐵) ∈ Fin)
3	1, 2	mpan2 692	1 ⊢ (𝐴 ∈ Fin → (𝐴 ∖ 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∈ wcel 2114   ∖ cdif 3886   ⊆ wss 3889  Fincfn 8893

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  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 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-om 7818  df-1o 8405  df-en 8894  df-fin 8897

This theorem is referenced by:  php  9141  dif1ennnALT  9187  fodomfir  9238  dif1card  9932  hashun2  14345  hashun3  14346  hashssdif  14374  hashdifpr  14377  hashfun  14399  hashf1lem2  14418  fsumsplit1  15707  fsumdifsnconst  15754  hash2iun1dif1  15787  incexc  15802  fprodeq0g  15959  fprodfvdvdsd  16303  ramub1lem1  16997  ramub1lem2  16998  prmdvdsprmo  17013  psgnprfval  19496  sylow2alem2  19593  sylow2a  19594  gsummgp0  20297  psgnfix1  21578  psgndiflemB  21580  psgndif  21582  copsgndif  21583  dmatmul  22462  submaval  22546  1marepvsma1  22548  gsummatr01lem3  22622  gsummatr01  22624  smadiadetlem3  22633  smadiadet  22635  cramerimplem1  22648  cmpcld  23367  alexsubALTlem3  24014  cldsubg  24076  xrge0gsumle  24799  amgm  26954  rpvmasum2  27475  numedglnl  29213  cusgrfilem3  29526  finsumvtxdg2ssteplem4  29617  finsumvtxdg2sstep  29618  diffib  32591  unidifsnel  32605  unidifsnne  32606  fprodeq02  32897  indsumin  32921  gsummptres  33113  cycpmconjslem2  33216  elrspunidl  33488  vietalem  33723  gsumesum  34203  ballotlemfp1  34636  ballotlemgun  34669  hgt750lemd  34792  hgt750lemb  34800  hgt750leme  34802  tgoldbachgtde  34804  subfacp1lem1  35361  subfacp1lem3  35364  topdifinfindis  37662  matunitlindflem1  37937  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem30  37971  aks6d1c5lem3  42576  aks6d1c5lem2  42577  unitscyglem4  42637  elrfi  43126  eldioph2lem1  43192  eldioph2lem2  43193  pellexlem5  43261  fsumnncl  46002  fprod0  46026  dvmptfprodlem  46372  stoweidlem44  46472  stoweidlem57  46485  fourierdlem42  46577  fourierdlem102  46636  fourierdlem114  46648  etransclem25  46687  etransclem35  46697  hspmbllem2  47055  fsummsndifre  47828  fsummmodsndifre  47830  isubgr3stgrlem2  48443  mgpsumunsn  48837  mgpsumz  48838  mgpsumn  48839