Theorem diffi 9144

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

Syntax hints:   → wi 4   ∈ wcel 2143   ∖ cdif 3902   ⊆ wss 3905  Fincfn 8928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7719

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-om 7848  df-1o 8438  df-en 8929  df-fin 8932

This theorem is referenced by:  php  9176  dif1ennnALT  9222  fodomfir  9273  dif1card  9967  hashun2  14397  hashun3  14398  hashssdif  14426  hashdifpr  14429  hashfun  14451  hashf1lem2  14470  fsumsplit1  15773  fsumdifsnconst  15820  hash2iun1dif1  15853  incexc  15868  fprodeq0g  16025  fprodfvdvdsd  16369  ramub1lem1  17063  ramub1lem2  17064  prmdvdsprmo  17079  psgnprfval  19562  sylow2alem2  19659  sylow2a  19660  gsummgp0  20367  psgnfix1  21651  psgndiflemB  21653  psgndif  21655  copsgndif  21656  dmatmul  22558  submaval  22642  1marepvsma1  22644  gsummatr01lem3  22718  gsummatr01  22720  smadiadetlem3  22729  smadiadet  22731  cramerimplem1  22744  cmpcld  23463  alexsubALTlem3  24110  cldsubg  24172  xrge0gsumle  24895  amgm  27056  rpvmasum2  27577  numedglnl  29346  cusgrfilem3  29659  finsumvtxdg2ssteplem4  29750  finsumvtxdg2sstep  29751  diffib  32721  unidifsnel  32735  unidifsnne  32736  fprodeq02  33027  indsumin  33040  gsummptres  33233  cycpmconjslem2  33336  elrspunidl  33615  vietalem  33877  gsumesum  34357  ballotlemfp1  34790  ballotlemgun  34823  hgt750lemd  34943  hgt750lemb  34951  hgt750leme  34953  tgoldbachgtde  34955  subfacp1lem1  35530  subfacp1lem3  35533  topdifinfindis  37841  matunitlindflem1  38116  poimirlem25  38145  poimirlem26  38146  poimirlem27  38147  poimirlem30  38150  aks6d1c5lem3  42755  aks6d1c5lem2  42756  unitscyglem4  42816  elrfi  43276  eldioph2lem1  43342  eldioph2lem2  43343  pellexlem5  43411  fsumnncl  46149  fprod0  46173  dvmptfprodlem  46519  stoweidlem44  46619  stoweidlem57  46632  fourierdlem42  46724  fourierdlem102  46783  fourierdlem114  46795  etransclem25  46834  etransclem35  46844  hspmbllem2  47202  fsummsndifre  47975  fsummmodsndifre  47977  isubgr3stgrlem2  48590  mgpsumunsn  48984  mgpsumz  48985  mgpsumn  48986