Theorem diffi 9238

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

Syntax hints:   → wi 4   ∈ wcel 2103   ∖ cdif 3967   ⊆ wss 3970  Fincfn 8999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pr 5450  ax-un 7766

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-pss 3990  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5170  df-opab 5232  df-tr 5287  df-id 5597  df-eprel 5603  df-po 5611  df-so 5612  df-fr 5654  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-ord 6397  df-on 6398  df-lim 6399  df-suc 6400  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-f1 6577  df-fo 6578  df-f1o 6579  df-fv 6580  df-om 7900  df-1o 8518  df-en 9000  df-fin 9003

This theorem is referenced by:  php  9269  dif1ennnALT  9335  fodomfir  9392  dif1card  10075  hashun2  14428  hashun3  14429  hashssdif  14457  hashdifpr  14460  hashfun  14482  hashf1lem2  14501  fsumsplit1  15789  fsumdifsnconst  15835  hash2iun1dif1  15868  incexc  15881  fprodeq0g  16036  fprodfvdvdsd  16376  ramub1lem1  17068  ramub1lem2  17069  prmdvdsprmo  17084  psgnprfval  19558  sylow2alem2  19655  sylow2a  19656  gsummgp0  20336  psgnfix1  21634  psgndiflemB  21636  psgndif  21638  copsgndif  21639  dmatmul  22517  submaval  22601  1marepvsma1  22603  gsummatr01lem3  22677  gsummatr01  22679  smadiadetlem3  22688  smadiadet  22690  cramerimplem1  22703  cmpcld  23424  alexsubALTlem3  24071  cldsubg  24133  xrge0gsumle  24867  amgm  27043  rpvmasum2  27565  numedglnl  29170  cusgrfilem3  29484  finsumvtxdg2ssteplem4  29575  finsumvtxdg2sstep  29576  diffib  32542  unidifsnel  32554  unidifsnne  32555  fprodeq02  32819  gsummptres  33027  cycpmconjslem2  33140  elrspunidl  33413  indsumin  33978  gsumesum  34015  ballotlemfp1  34448  ballotlemgun  34481  hgt750lemd  34617  hgt750lemb  34625  hgt750leme  34627  tgoldbachgtde  34629  subfacp1lem1  35139  subfacp1lem3  35142  topdifinfindis  37260  matunitlindflem1  37524  poimirlem25  37553  poimirlem26  37554  poimirlem27  37555  poimirlem30  37558  aks6d1c5lem3  42042  aks6d1c5lem2  42043  unitscyglem4  42103  elrfi  42587  eldioph2lem1  42653  eldioph2lem2  42654  pellexlem5  42726  fsumnncl  45427  fprod0  45451  dvmptfprodlem  45799  stoweidlem44  45899  stoweidlem57  45912  fourierdlem42  46004  fourierdlem102  46063  fourierdlem114  46075  etransclem25  46114  etransclem35  46124  hspmbllem2  46482  fsummsndifre  47178  fsummmodsndifre  47180  mgpsumunsn  48004  mgpsumz  48005  mgpsumn  48006