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

Theorem imass1 5402
Description: Subset theorem for image. (Contributed by NM, 16-Mar-2004.)
Assertion
Ref Expression
imass1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))

Proof of Theorem imass1
StepHypRef Expression
1 ssres 5327 . . 3 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
2 rnss 5258 . . 3 ((𝐴𝐶) ⊆ (𝐵𝐶) → ran (𝐴𝐶) ⊆ ran (𝐵𝐶))
31, 2syl 17 . 2 (𝐴𝐵 → ran (𝐴𝐶) ⊆ ran (𝐵𝐶))
4 df-ima 5037 . 2 (𝐴𝐶) = ran (𝐴𝐶)
5 df-ima 5037 . 2 (𝐵𝐶) = ran (𝐵𝐶)
63, 4, 53sstr4g 3604 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3535  ran crn 5025  cres 5026  cima 5027
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-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-opab 4634  df-cnv 5032  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037
This theorem is referenced by:  vdwnnlem1  15479  dprdres  18192  imasnopn  21241  imasncld  21242  imasncls  21243  utoptop  21786  restutop  21789  ustuqtop3  21795  utopreg  21804  metustbl  22118  imadifxp  28598  esum2d  29284  eulerpartlemmf  29566  brtrclfv2  36837  frege97d  36862  frege109d  36867  frege131d  36874  hess  36893
  Copyright terms: Public domain W3C validator