Theorem diffi 8927

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∖ cdif 3888   ⊆ wss 3891  Fincfn 8707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-om 7701  df-1o 8281  df-en 8708  df-fin 8711

This theorem is referenced by:  php  8957  dif1enALT  9011  unfiOLD  9042  dif1card  9750  hashun2  14079  hashun3  14080  hashssdif  14108  hashdifpr  14111  hashfun  14133  hashf1lem2  14151  fsumsplit1  15438  fsumdifsnconst  15484  hash2iun1dif1  15517  incexc  15530  fprodeq0g  15685  fprodfvdvdsd  16024  ramub1lem1  16708  ramub1lem2  16709  prmdvdsprmo  16724  psgnprfval  19110  sylow2alem2  19204  sylow2a  19205  gsummgp0  19828  psgnfix1  20784  psgndiflemB  20786  psgndif  20788  copsgndif  20789  dmatmul  21627  submaval  21711  1marepvsma1  21713  gsummatr01lem3  21787  gsummatr01  21789  smadiadetlem3  21798  smadiadet  21800  cramerimplem1  21813  cmpcld  22534  alexsubALTlem3  23181  cldsubg  23243  xrge0gsumle  23977  amgm  26121  rpvmasum2  26641  numedglnl  27495  cusgrfilem3  27805  finsumvtxdg2ssteplem4  27896  finsumvtxdg2sstep  27897  diffib  30848  unidifsnel  30862  unidifsnne  30863  fprodeq02  31116  gsummptres  31291  cycpmconjslem2  31401  elrspunidl  31585  indsumin  31969  gsumesum  32006  ballotlemfp1  32437  ballotlemgun  32470  hgt750lemd  32607  hgt750lemb  32615  hgt750leme  32617  tgoldbachgtde  32619  subfacp1lem1  33120  subfacp1lem3  33123  topdifinfindis  35496  matunitlindflem1  35752  poimirlem25  35781  poimirlem26  35782  poimirlem27  35783  poimirlem30  35786  elrfi  40496  eldioph2lem1  40562  eldioph2lem2  40563  pellexlem5  40635  fsumnncl  43067  fprod0  43091  dvmptfprodlem  43439  stoweidlem44  43539  stoweidlem57  43552  fourierdlem42  43644  fourierdlem102  43703  fourierdlem114  43715  etransclem25  43754  etransclem35  43764  hspmbllem2  44119  fsummsndifre  44776  fsummmodsndifre  44778  mgpsumunsn  45649  mgpsumz  45650  mgpsumn  45651