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

Theorem imass2 5959
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 5875 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 rnss 5803 . . 3 ((𝐶𝐴) ⊆ (𝐶𝐵) → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
31, 2syl 17 . 2 (𝐴𝐵 → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
4 df-ima 5562 . 2 (𝐶𝐴) = ran (𝐶𝐴)
5 df-ima 5562 . 2 (𝐶𝐵) = ran (𝐶𝐵)
63, 4, 53sstr4g 4011 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3935  ran crn 5550  cres 5551  cima 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-xp 5555  df-cnv 5557  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562
This theorem is referenced by:  funimass1  6430  funimass2  6431  fvimacnv  6816  fnfvimad  6987  f1imass  7013  ecinxp  8362  sbthlem1  8616  sbthlem2  8617  php3  8692  ordtypelem2  8972  tcrank  9302  limsupgord  14819  isercoll  15014  isacs1i  16918  gsumzf1o  18963  dprdres  19081  dprd2da  19095  dmdprdsplit2lem  19098  lmhmlsp  19752  f1lindf  20896  iscnp4  21801  cnpco  21805  cncls2i  21808  cnntri  21809  cnrest2  21824  cnpresti  21826  cnprest  21827  1stcfb  21983  xkococnlem  22197  qtopval2  22234  tgqtop  22250  qtoprest  22255  kqdisj  22270  regr1lem  22277  kqreglem1  22279  kqreglem2  22280  kqnrmlem1  22281  kqnrmlem2  22282  nrmhmph  22332  fbasrn  22422  elfm2  22486  fmfnfmlem1  22492  fmco  22499  flffbas  22533  cnpflf2  22538  cnextcn  22605  metcnp3  23079  metustto  23092  cfilucfil  23098  uniioombllem3  24115  dyadmbllem  24129  mbfconstlem  24157  i1fima2  24209  itg2gt0  24290  ellimc3  24406  limcflf  24408  limcresi  24412  limciun  24421  lhop  24542  ig1peu  24694  ig1pdvds  24699  psercnlem2  24941  dvloglem  25158  efopn  25168  fnpreimac  30345  txomap  30998  tpr2rico  31055  pthhashvtx  32272  cvmsss2  32419  cvmopnlem  32423  cvmliftmolem1  32426  cvmliftlem15  32443  cvmlift2lem9  32456  imadifss  34749  poimirlem1  34775  poimirlem2  34776  poimirlem3  34777  poimirlem15  34789  poimirlem30  34804  dvtan  34824  heibor1lem  34970  isnumbasabl  39586  isnumbasgrp  39587  dfacbasgrp  39588  trclimalb2  39951  frege81d  39972  imass2d  41416  limccog  41781  liminfgord  41915
  Copyright terms: Public domain W3C validator