Theorem diffi 9089

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∖ cdif 3900   ⊆ wss 3903  Fincfn 8872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-om 7800  df-1o 8388  df-en 8873  df-fin 8876

This theorem is referenced by:  php  9121  dif1ennnALT  9166  fodomfir  9218  dif1card  9904  hashun2  14290  hashun3  14291  hashssdif  14319  hashdifpr  14322  hashfun  14344  hashf1lem2  14363  fsumsplit1  15652  fsumdifsnconst  15698  hash2iun1dif1  15731  incexc  15744  fprodeq0g  15901  fprodfvdvdsd  16245  ramub1lem1  16938  ramub1lem2  16939  prmdvdsprmo  16954  psgnprfval  19400  sylow2alem2  19497  sylow2a  19498  gsummgp0  20203  psgnfix1  21505  psgndiflemB  21507  psgndif  21509  copsgndif  21510  dmatmul  22382  submaval  22466  1marepvsma1  22468  gsummatr01lem3  22542  gsummatr01  22544  smadiadetlem3  22553  smadiadet  22555  cramerimplem1  22568  cmpcld  23287  alexsubALTlem3  23934  cldsubg  23996  xrge0gsumle  24720  amgm  26899  rpvmasum2  27421  numedglnl  29089  cusgrfilem3  29403  finsumvtxdg2ssteplem4  29494  finsumvtxdg2sstep  29495  diffib  32465  unidifsnel  32479  unidifsnne  32480  fprodeq02  32769  indsumin  32806  gsummptres  33006  cycpmconjslem2  33098  elrspunidl  33366  gsumesum  34032  ballotlemfp1  34466  ballotlemgun  34499  hgt750lemd  34622  hgt750lemb  34630  hgt750leme  34632  tgoldbachgtde  34634  subfacp1lem1  35162  subfacp1lem3  35165  topdifinfindis  37330  matunitlindflem1  37606  poimirlem25  37635  poimirlem26  37636  poimirlem27  37637  poimirlem30  37640  aks6d1c5lem3  42120  aks6d1c5lem2  42121  unitscyglem4  42181  elrfi  42677  eldioph2lem1  42743  eldioph2lem2  42744  pellexlem5  42816  fsumnncl  45563  fprod0  45587  dvmptfprodlem  45935  stoweidlem44  46035  stoweidlem57  46048  fourierdlem42  46140  fourierdlem102  46199  fourierdlem114  46211  etransclem25  46250  etransclem35  46260  hspmbllem2  46618  fsummsndifre  47366  fsummmodsndifre  47368  isubgr3stgrlem2  47961  mgpsumunsn  48355  mgpsumz  48356  mgpsumn  48357