Theorem diffi 9194

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∖ cdif 3928   ⊆ wss 3931  Fincfn 8964

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-om 7867  df-1o 8485  df-en 8965  df-fin 8968

This theorem is referenced by:  php  9226  dif1ennnALT  9288  fodomfir  9345  dif1card  10029  hashun2  14406  hashun3  14407  hashssdif  14435  hashdifpr  14438  hashfun  14460  hashf1lem2  14479  fsumsplit1  15766  fsumdifsnconst  15812  hash2iun1dif1  15845  incexc  15858  fprodeq0g  16015  fprodfvdvdsd  16358  ramub1lem1  17051  ramub1lem2  17052  prmdvdsprmo  17067  psgnprfval  19507  sylow2alem2  19604  sylow2a  19605  gsummgp0  20283  psgnfix1  21563  psgndiflemB  21565  psgndif  21567  copsgndif  21568  dmatmul  22440  submaval  22524  1marepvsma1  22526  gsummatr01lem3  22600  gsummatr01  22602  smadiadetlem3  22611  smadiadet  22613  cramerimplem1  22626  cmpcld  23345  alexsubALTlem3  23992  cldsubg  24054  xrge0gsumle  24778  amgm  26958  rpvmasum2  27480  numedglnl  29128  cusgrfilem3  29442  finsumvtxdg2ssteplem4  29533  finsumvtxdg2sstep  29534  diffib  32507  unidifsnel  32521  unidifsnne  32522  fprodeq02  32807  indsumin  32844  gsummptres  33051  cycpmconjslem2  33171  elrspunidl  33448  gsumesum  34095  ballotlemfp1  34529  ballotlemgun  34562  hgt750lemd  34685  hgt750lemb  34693  hgt750leme  34695  tgoldbachgtde  34697  subfacp1lem1  35206  subfacp1lem3  35209  topdifinfindis  37369  matunitlindflem1  37645  poimirlem25  37674  poimirlem26  37675  poimirlem27  37676  poimirlem30  37679  aks6d1c5lem3  42155  aks6d1c5lem2  42156  unitscyglem4  42216  elrfi  42692  eldioph2lem1  42758  eldioph2lem2  42759  pellexlem5  42831  fsumnncl  45581  fprod0  45605  dvmptfprodlem  45953  stoweidlem44  46053  stoweidlem57  46066  fourierdlem42  46158  fourierdlem102  46217  fourierdlem114  46229  etransclem25  46268  etransclem35  46278  hspmbllem2  46636  fsummsndifre  47366  fsummmodsndifre  47368  isubgr3stgrlem2  47959  mgpsumunsn  48316  mgpsumz  48317  mgpsumn  48318