Theorem diffi 9130

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∖ cdif 3910   ⊆ wss 3913  Fincfn 8890

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-om 7808  df-1o 8417  df-en 8891  df-fin 8894

This theorem is referenced by:  php  9161  dif1ennnALT  9228  unfiOLD  9264  dif1card  9955  hashun2  14293  hashun3  14294  hashssdif  14322  hashdifpr  14325  hashfun  14347  hashf1lem2  14367  fsumsplit1  15641  fsumdifsnconst  15687  hash2iun1dif1  15720  incexc  15733  fprodeq0g  15888  fprodfvdvdsd  16227  ramub1lem1  16909  ramub1lem2  16910  prmdvdsprmo  16925  psgnprfval  19317  sylow2alem2  19414  sylow2a  19415  gsummgp0  20046  psgnfix1  21039  psgndiflemB  21041  psgndif  21043  copsgndif  21044  dmatmul  21883  submaval  21967  1marepvsma1  21969  gsummatr01lem3  22043  gsummatr01  22045  smadiadetlem3  22054  smadiadet  22056  cramerimplem1  22069  cmpcld  22790  alexsubALTlem3  23437  cldsubg  23499  xrge0gsumle  24233  amgm  26377  rpvmasum2  26897  numedglnl  28158  cusgrfilem3  28468  finsumvtxdg2ssteplem4  28559  finsumvtxdg2sstep  28560  diffib  31512  unidifsnel  31526  unidifsnne  31527  fprodeq02  31789  gsummptres  31964  cycpmconjslem2  32074  elrspunidl  32279  indsumin  32710  gsumesum  32747  ballotlemfp1  33180  ballotlemgun  33213  hgt750lemd  33350  hgt750lemb  33358  hgt750leme  33360  tgoldbachgtde  33362  subfacp1lem1  33860  subfacp1lem3  33863  topdifinfindis  35890  matunitlindflem1  36147  poimirlem25  36176  poimirlem26  36177  poimirlem27  36178  poimirlem30  36181  elrfi  41075  eldioph2lem1  41141  eldioph2lem2  41142  pellexlem5  41214  fsumnncl  43933  fprod0  43957  dvmptfprodlem  44305  stoweidlem44  44405  stoweidlem57  44418  fourierdlem42  44510  fourierdlem102  44569  fourierdlem114  44581  etransclem25  44620  etransclem35  44630  hspmbllem2  44988  fsummsndifre  45684  fsummmodsndifre  45686  mgpsumunsn  46557  mgpsumz  46558  mgpsumn  46559