Theorem diffi 9202

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

Syntax hints:   → wi 4   ∈ wcel 2098   ∖ cdif 3942   ⊆ wss 3945  Fincfn 8962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pr 5428  ax-un 7739

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-om 7870  df-1o 8485  df-en 8963  df-fin 8966

This theorem is referenced by:  php  9233  dif1ennnALT  9300  unfiOLD  9336  dif1card  10033  hashun2  14374  hashun3  14375  hashssdif  14403  hashdifpr  14406  hashfun  14428  hashf1lem2  14449  fsumsplit1  15723  fsumdifsnconst  15769  hash2iun1dif1  15802  incexc  15815  fprodeq0g  15970  fprodfvdvdsd  16310  ramub1lem1  16994  ramub1lem2  16995  prmdvdsprmo  17010  psgnprfval  19480  sylow2alem2  19577  sylow2a  19578  gsummgp0  20258  psgnfix1  21534  psgndiflemB  21536  psgndif  21538  copsgndif  21539  dmatmul  22429  submaval  22513  1marepvsma1  22515  gsummatr01lem3  22589  gsummatr01  22591  smadiadetlem3  22600  smadiadet  22602  cramerimplem1  22615  cmpcld  23336  alexsubALTlem3  23983  cldsubg  24045  xrge0gsumle  24779  amgm  26953  rpvmasum2  27475  numedglnl  29013  cusgrfilem3  29327  finsumvtxdg2ssteplem4  29418  finsumvtxdg2sstep  29419  diffib  32375  unidifsnel  32388  unidifsnne  32389  fprodeq02  32643  gsummptres  32823  cycpmconjslem2  32933  elrspunidl  33206  indsumin  33711  gsumesum  33748  ballotlemfp1  34181  ballotlemgun  34214  hgt750lemd  34350  hgt750lemb  34358  hgt750leme  34360  tgoldbachgtde  34362  subfacp1lem1  34859  subfacp1lem3  34862  topdifinfindis  36895  matunitlindflem1  37159  poimirlem25  37188  poimirlem26  37189  poimirlem27  37190  poimirlem30  37193  aks6d1c5lem3  41677  aks6d1c5lem2  41678  elrfi  42179  eldioph2lem1  42245  eldioph2lem2  42246  pellexlem5  42318  fsumnncl  45023  fprod0  45047  dvmptfprodlem  45395  stoweidlem44  45495  stoweidlem57  45508  fourierdlem42  45600  fourierdlem102  45659  fourierdlem114  45671  etransclem25  45710  etransclem35  45720  hspmbllem2  46078  fsummsndifre  46775  fsummmodsndifre  46777  mgpsumunsn  47537  mgpsumz  47538  mgpsumn  47539