Theorem diffi 9185

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

Syntax hints:   → wi 4   ∈ wcel 2105   ∖ cdif 3945   ⊆ wss 3948  Fincfn 8945

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7860  df-1o 8472  df-en 8946  df-fin 8949

This theorem is referenced by:  php  9216  dif1ennnALT  9283  unfiOLD  9319  dif1card  10011  hashun2  14350  hashun3  14351  hashssdif  14379  hashdifpr  14382  hashfun  14404  hashf1lem2  14424  fsumsplit1  15698  fsumdifsnconst  15744  hash2iun1dif1  15777  incexc  15790  fprodeq0g  15945  fprodfvdvdsd  16284  ramub1lem1  16966  ramub1lem2  16967  prmdvdsprmo  16982  psgnprfval  19437  sylow2alem2  19534  sylow2a  19535  gsummgp0  20213  psgnfix1  21461  psgndiflemB  21463  psgndif  21465  copsgndif  21466  dmatmul  22319  submaval  22403  1marepvsma1  22405  gsummatr01lem3  22479  gsummatr01  22481  smadiadetlem3  22490  smadiadet  22492  cramerimplem1  22505  cmpcld  23226  alexsubALTlem3  23873  cldsubg  23935  xrge0gsumle  24669  amgm  26837  rpvmasum2  27359  numedglnl  28838  cusgrfilem3  29148  finsumvtxdg2ssteplem4  29239  finsumvtxdg2sstep  29240  diffib  32193  unidifsnel  32206  unidifsnne  32207  fprodeq02  32463  gsummptres  32641  cycpmconjslem2  32751  elrspunidl  32987  indsumin  33485  gsumesum  33522  ballotlemfp1  33955  ballotlemgun  33988  hgt750lemd  34125  hgt750lemb  34133  hgt750leme  34135  tgoldbachgtde  34137  subfacp1lem1  34635  subfacp1lem3  34638  topdifinfindis  36693  matunitlindflem1  36950  poimirlem25  36979  poimirlem26  36980  poimirlem27  36981  poimirlem30  36984  elrfi  41897  eldioph2lem1  41963  eldioph2lem2  41964  pellexlem5  42036  fsumnncl  44749  fprod0  44773  dvmptfprodlem  45121  stoweidlem44  45221  stoweidlem57  45234  fourierdlem42  45326  fourierdlem102  45385  fourierdlem114  45397  etransclem25  45436  etransclem35  45446  hspmbllem2  45804  fsummsndifre  46501  fsummmodsndifre  46503  mgpsumunsn  47202  mgpsumz  47203  mgpsumn  47204