Theorem diffi 9084

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∖ cdif 3894   ⊆ wss 3897  Fincfn 8869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-om 7797  df-1o 8385  df-en 8870  df-fin 8873

This theorem is referenced by:  php  9116  dif1ennnALT  9161  fodomfir  9212  dif1card  9901  hashun2  14290  hashun3  14291  hashssdif  14319  hashdifpr  14322  hashfun  14344  hashf1lem2  14363  fsumsplit1  15652  fsumdifsnconst  15698  hash2iun1dif1  15731  incexc  15744  fprodeq0g  15901  fprodfvdvdsd  16245  ramub1lem1  16938  ramub1lem2  16939  prmdvdsprmo  16954  psgnprfval  19433  sylow2alem2  19530  sylow2a  19531  gsummgp0  20236  psgnfix1  21535  psgndiflemB  21537  psgndif  21539  copsgndif  21540  dmatmul  22412  submaval  22496  1marepvsma1  22498  gsummatr01lem3  22572  gsummatr01  22574  smadiadetlem3  22583  smadiadet  22585  cramerimplem1  22598  cmpcld  23317  alexsubALTlem3  23964  cldsubg  24026  xrge0gsumle  24749  amgm  26928  rpvmasum2  27450  numedglnl  29122  cusgrfilem3  29436  finsumvtxdg2ssteplem4  29527  finsumvtxdg2sstep  29528  diffib  32501  unidifsnel  32515  unidifsnne  32516  fprodeq02  32806  indsumin  32843  gsummptres  33032  cycpmconjslem2  33124  elrspunidl  33393  gsumesum  34072  ballotlemfp1  34505  ballotlemgun  34538  hgt750lemd  34661  hgt750lemb  34669  hgt750leme  34671  tgoldbachgtde  34673  subfacp1lem1  35223  subfacp1lem3  35226  topdifinfindis  37390  matunitlindflem1  37666  poimirlem25  37695  poimirlem26  37696  poimirlem27  37697  poimirlem30  37700  aks6d1c5lem3  42240  aks6d1c5lem2  42241  unitscyglem4  42301  elrfi  42797  eldioph2lem1  42863  eldioph2lem2  42864  pellexlem5  42936  fsumnncl  45682  fprod0  45706  dvmptfprodlem  46052  stoweidlem44  46152  stoweidlem57  46165  fourierdlem42  46257  fourierdlem102  46316  fourierdlem114  46328  etransclem25  46367  etransclem35  46377  hspmbllem2  46735  fsummsndifre  47482  fsummmodsndifre  47484  isubgr3stgrlem2  48077  mgpsumunsn  48471  mgpsumz  48472  mgpsumn  48473