MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  diffi Structured version   Visualization version   GIF version

Theorem diffi 8050
Description: If 𝐴 is finite, (𝐴𝐵) is finite. (Contributed by FL, 3-Aug-2009.)
Assertion
Ref Expression
diffi (𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin)

Proof of Theorem diffi
StepHypRef Expression
1 difss 3694 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssfi 8038 . 2 ((𝐴 ∈ Fin ∧ (𝐴𝐵) ⊆ 𝐴) → (𝐴𝐵) ∈ Fin)
31, 2mpan2 702 1 (𝐴 ∈ Fin → (𝐴𝐵) ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1975  cdif 3532  wss 3535  Fincfn 7814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-sbc 3398  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-om 6931  df-er 7602  df-en 7815  df-fin 7818
This theorem is referenced by:  dif1en  8051  unfi  8085  dif1card  8689  hashun2  12981  hashun3  12982  hashssdif  13009  hashdifpr  13012  hashfun  13032  hashf1lem2  13045  incexc  14350  fprodeq0g  14506  fprodfvdvdsd  14838  ramub1lem1  15510  ramub1lem2  15511  prmdvdsprmo  15526  psgnprfval  17706  sylow2alem2  17798  sylow2a  17799  gsummgp0  18373  psgnfix1  19704  psgndiflemB  19706  psgndif  19708  zrhcopsgndif  19709  dmatmul  20060  submaval  20144  1marepvsma1  20146  gsummatr01lem3  20220  gsummatr01  20222  smadiadetlem3  20231  smadiadet  20233  cramerimplem1  20246  cmpcld  20953  alexsubALTlem3  21601  cldsubg  21662  xrge0gsumle  22372  amgm  24430  rpvmasum2  24914  cusgrafilem3  25771  frghash2spot  26352  usgreghash2spotv  26355  gsummptres  28917  gsumesum  29250  ballotlemfp1  29682  ballotlemgun  29715  subfacp1lem1  30217  subfacp1lem3  30220  topdifinfindis  32169  matunitlindflem1  32374  poimirlem25  32403  poimirlem26  32404  poimirlem27  32405  poimirlem30  32408  elrfi  36074  eldioph2lem1  36140  eldioph2lem2  36141  pellexlem5  36214  fsumnncl  38438  fsumsplit1  38439  fprod0  38463  dvmptfprodlem  38634  stoweidlem44  38737  stoweidlem57  38750  fourierdlem42  38842  fourierdlem102  38901  fourierdlem114  38913  etransclem25  38952  etransclem35  38962  hspmbllem2  39317  fsummsndifre  40217  fsummmodsndifre  40219  cusgrfilem3  40671  frgrhash2wsp  41495  fusgreghash2wspv  41497  mgpsumunsn  41931  mgpsumz  41932  mgpsumn  41933
  Copyright terms: Public domain W3C validator