Theorem diffi 8786

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∖ cdif 3855   ⊆ wss 3858  Fincfn 8527

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-om 7580  df-1o 8112  df-en 8528  df-fin 8531

This theorem is referenced by:  dif1enOLD  8787  unfiOLD  8818  dif1card  9470  hashun2  13794  hashun3  13795  hashssdif  13823  hashdifpr  13826  hashfun  13848  hashf1lem2  13866  fsumdifsnconst  15194  hash2iun1dif1  15227  incexc  15240  fprodeq0g  15396  fprodfvdvdsd  15735  ramub1lem1  16417  ramub1lem2  16418  prmdvdsprmo  16433  psgnprfval  18716  sylow2alem2  18810  sylow2a  18811  gsummgp0  19429  psgnfix1  20363  psgndiflemB  20365  psgndif  20367  copsgndif  20368  dmatmul  21197  submaval  21281  1marepvsma1  21283  gsummatr01lem3  21357  gsummatr01  21359  smadiadetlem3  21368  smadiadet  21370  cramerimplem1  21383  cmpcld  22102  alexsubALTlem3  22749  cldsubg  22811  xrge0gsumle  23534  amgm  25675  rpvmasum2  26195  numedglnl  27036  cusgrfilem3  27346  finsumvtxdg2ssteplem4  27437  finsumvtxdg2sstep  27438  diffib  30391  unidifsnel  30405  unidifsnne  30406  fprodeq02  30661  gsummptres  30838  cycpmconjslem2  30948  elrspunidl  31127  indsumin  31509  gsumesum  31546  ballotlemfp1  31977  ballotlemgun  32010  hgt750lemd  32147  hgt750lemb  32155  hgt750leme  32157  tgoldbachgtde  32159  subfacp1lem1  32657  subfacp1lem3  32660  topdifinfindis  35043  matunitlindflem1  35333  poimirlem25  35362  poimirlem26  35363  poimirlem27  35364  poimirlem30  35367  elrfi  40008  eldioph2lem1  40074  eldioph2lem2  40075  pellexlem5  40147  fsumnncl  42579  fsumsplit1  42580  fprod0  42604  dvmptfprodlem  42952  stoweidlem44  43052  stoweidlem57  43065  fourierdlem42  43157  fourierdlem102  43216  fourierdlem114  43228  etransclem25  43267  etransclem35  43277  hspmbllem2  43632  fsummsndifre  44257  fsummmodsndifre  44259  mgpsumunsn  45130  mgpsumz  45131  mgpsumn  45132