Theorem diffi 9000

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

Syntax hints:   → wi 4   ∈ wcel 2104   ∖ cdif 3889   ⊆ wss 3892  Fincfn 8764

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-om 7745  df-1o 8328  df-en 8765  df-fin 8768

This theorem is referenced by:  php  9031  dif1enALT  9094  unfiOLD  9125  dif1card  9812  hashun2  14143  hashun3  14144  hashssdif  14172  hashdifpr  14175  hashfun  14197  hashf1lem2  14215  fsumsplit1  15502  fsumdifsnconst  15548  hash2iun1dif1  15581  incexc  15594  fprodeq0g  15749  fprodfvdvdsd  16088  ramub1lem1  16772  ramub1lem2  16773  prmdvdsprmo  16788  psgnprfval  19174  sylow2alem2  19268  sylow2a  19269  gsummgp0  19892  psgnfix1  20848  psgndiflemB  20850  psgndif  20852  copsgndif  20853  dmatmul  21691  submaval  21775  1marepvsma1  21777  gsummatr01lem3  21851  gsummatr01  21853  smadiadetlem3  21862  smadiadet  21864  cramerimplem1  21877  cmpcld  22598  alexsubALTlem3  23245  cldsubg  23307  xrge0gsumle  24041  amgm  26185  rpvmasum2  26705  numedglnl  27559  cusgrfilem3  27869  finsumvtxdg2ssteplem4  27960  finsumvtxdg2sstep  27961  diffib  30914  unidifsnel  30928  unidifsnne  30929  fprodeq02  31182  gsummptres  31357  cycpmconjslem2  31467  elrspunidl  31651  indsumin  32035  gsumesum  32072  ballotlemfp1  32503  ballotlemgun  32536  hgt750lemd  32673  hgt750lemb  32681  hgt750leme  32683  tgoldbachgtde  32685  subfacp1lem1  33186  subfacp1lem3  33189  topdifinfindis  35561  matunitlindflem1  35817  poimirlem25  35846  poimirlem26  35847  poimirlem27  35848  poimirlem30  35851  elrfi  40553  eldioph2lem1  40619  eldioph2lem2  40620  pellexlem5  40692  fsumnncl  43162  fprod0  43186  dvmptfprodlem  43534  stoweidlem44  43634  stoweidlem57  43647  fourierdlem42  43739  fourierdlem102  43798  fourierdlem114  43810  etransclem25  43849  etransclem35  43859  hspmbllem2  44215  fsummsndifre  44882  fsummmodsndifre  44884  mgpsumunsn  45755  mgpsumz  45756  mgpsumn  45757