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

Theorem imass2 5489
Description: Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
imass2 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))

Proof of Theorem imass2
StepHypRef Expression
1 ssres2 5413 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 rnss 5343 . . 3 ((𝐶𝐴) ⊆ (𝐶𝐵) → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
31, 2syl 17 . 2 (𝐴𝐵 → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
4 df-ima 5117 . 2 (𝐶𝐴) = ran (𝐶𝐴)
5 df-ima 5117 . 2 (𝐶𝐵) = ran (𝐶𝐵)
63, 4, 53sstr4g 3638 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3567  ran crn 5105  cres 5106  cima 5107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110  df-cnv 5112  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117
This theorem is referenced by:  funimass1  5959  funimass2  5960  fvimacnv  6318  f1imass  6506  ecinxp  7807  sbthlem1  8055  sbthlem2  8056  php3  8131  ordtypelem2  8409  tcrank  8732  limsupgord  14184  isercoll  14379  isacs1i  16299  gsumzf1o  18294  dprdres  18408  dprd2da  18422  dmdprdsplit2lem  18425  lmhmlsp  19030  f1lindf  20142  iscnp4  21048  cnpco  21052  cncls2i  21055  cnntri  21056  cnrest2  21071  cnpresti  21073  cnprest  21074  1stcfb  21229  xkococnlem  21443  qtopval2  21480  tgqtop  21496  qtoprest  21501  kqdisj  21516  regr1lem  21523  kqreglem1  21525  kqreglem2  21526  kqnrmlem1  21527  kqnrmlem2  21528  nrmhmph  21578  fbasrn  21669  elfm2  21733  fmfnfmlem1  21739  fmco  21746  flffbas  21780  cnpflf2  21785  cnextcn  21852  metcnp3  22326  metustto  22339  cfilucfil  22345  uniioombllem3  23334  dyadmbllem  23348  mbfconstlem  23377  i1fima2  23427  itg2gt0  23508  ellimc3  23624  limcflf  23626  limcresi  23630  limciun  23639  lhop  23760  ig1peu  23912  ig1pdvds  23917  psercnlem2  24159  dvloglem  24375  efopn  24385  txomap  29875  tpr2rico  29932  cvmsss2  31230  cvmopnlem  31234  cvmliftmolem1  31237  cvmliftlem15  31254  cvmlift2lem9  31267  imadifss  33355  poimirlem1  33381  poimirlem2  33382  poimirlem3  33383  poimirlem15  33395  poimirlem30  33410  dvtan  33431  heibor1lem  33579  isnumbasabl  37495  isnumbasgrp  37496  dfacbasgrp  37497  trclimalb2  37837  frege81d  37858  fnfvimad  39275  fnfvima2  39294  imass2d  39296  limccog  39652  liminfgord  39780
  Copyright terms: Public domain W3C validator