Theorem diffi 9111

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∖ cdif 3900   ⊆ wss 3903  Fincfn 8895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-om 7819  df-1o 8407  df-en 8896  df-fin 8899

This theorem is referenced by:  php  9143  dif1ennnALT  9189  fodomfir  9240  dif1card  9932  hashun2  14318  hashun3  14319  hashssdif  14347  hashdifpr  14350  hashfun  14372  hashf1lem2  14391  fsumsplit1  15680  fsumdifsnconst  15726  hash2iun1dif1  15759  incexc  15772  fprodeq0g  15929  fprodfvdvdsd  16273  ramub1lem1  16966  ramub1lem2  16967  prmdvdsprmo  16982  psgnprfval  19465  sylow2alem2  19562  sylow2a  19563  gsummgp0  20268  psgnfix1  21568  psgndiflemB  21570  psgndif  21572  copsgndif  21573  dmatmul  22456  submaval  22540  1marepvsma1  22542  gsummatr01lem3  22616  gsummatr01  22618  smadiadetlem3  22627  smadiadet  22629  cramerimplem1  22642  cmpcld  23361  alexsubALTlem3  24008  cldsubg  24070  xrge0gsumle  24793  amgm  26972  rpvmasum2  27494  numedglnl  29233  cusgrfilem3  29547  finsumvtxdg2ssteplem4  29638  finsumvtxdg2sstep  29639  diffib  32612  unidifsnel  32626  unidifsnne  32627  fprodeq02  32919  indsumin  32958  gsummptres  33150  cycpmconjslem2  33253  elrspunidl  33525  vietalem  33760  gsumesum  34241  ballotlemfp1  34674  ballotlemgun  34707  hgt750lemd  34830  hgt750lemb  34838  hgt750leme  34840  tgoldbachgtde  34842  subfacp1lem1  35399  subfacp1lem3  35402  topdifinfindis  37605  matunitlindflem1  37871  poimirlem25  37900  poimirlem26  37901  poimirlem27  37902  poimirlem30  37905  aks6d1c5lem3  42511  aks6d1c5lem2  42512  unitscyglem4  42572  elrfi  43055  eldioph2lem1  43121  eldioph2lem2  43122  pellexlem5  43194  fsumnncl  45936  fprod0  45960  dvmptfprodlem  46306  stoweidlem44  46406  stoweidlem57  46419  fourierdlem42  46511  fourierdlem102  46570  fourierdlem114  46582  etransclem25  46621  etransclem35  46631  hspmbllem2  46989  fsummsndifre  47736  fsummmodsndifre  47738  isubgr3stgrlem2  48331  mgpsumunsn  48725  mgpsumz  48726  mgpsumn  48727