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

Theorem imass2 5659
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 5583 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 rnss 5509 . . 3 ((𝐶𝐴) ⊆ (𝐶𝐵) → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
31, 2syl 17 . 2 (𝐴𝐵 → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
4 df-ima 5279 . 2 (𝐶𝐴) = ran (𝐶𝐴)
5 df-ima 5279 . 2 (𝐶𝐵) = ran (𝐶𝐵)
63, 4, 53sstr4g 3787 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3715  ran crn 5267  cres 5268  cima 5269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279
This theorem is referenced by:  funimass1  6132  funimass2  6133  fvimacnv  6495  f1imass  6684  ecinxp  7989  sbthlem1  8235  sbthlem2  8236  php3  8311  ordtypelem2  8589  tcrank  8920  limsupgord  14402  isercoll  14597  isacs1i  16519  gsumzf1o  18513  dprdres  18627  dprd2da  18641  dmdprdsplit2lem  18644  lmhmlsp  19251  f1lindf  20363  iscnp4  21269  cnpco  21273  cncls2i  21276  cnntri  21277  cnrest2  21292  cnpresti  21294  cnprest  21295  1stcfb  21450  xkococnlem  21664  qtopval2  21701  tgqtop  21717  qtoprest  21722  kqdisj  21737  regr1lem  21744  kqreglem1  21746  kqreglem2  21747  kqnrmlem1  21748  kqnrmlem2  21749  nrmhmph  21799  fbasrn  21889  elfm2  21953  fmfnfmlem1  21959  fmco  21966  flffbas  22000  cnpflf2  22005  cnextcn  22072  metcnp3  22546  metustto  22559  cfilucfil  22565  uniioombllem3  23553  dyadmbllem  23567  mbfconstlem  23595  i1fima2  23645  itg2gt0  23726  ellimc3  23842  limcflf  23844  limcresi  23848  limciun  23857  lhop  23978  ig1peu  24130  ig1pdvds  24135  psercnlem2  24377  dvloglem  24593  efopn  24603  txomap  30210  tpr2rico  30267  cvmsss2  31563  cvmopnlem  31567  cvmliftmolem1  31570  cvmliftlem15  31587  cvmlift2lem9  31600  imadifss  33697  poimirlem1  33723  poimirlem2  33724  poimirlem3  33725  poimirlem15  33737  poimirlem30  33752  dvtan  33773  heibor1lem  33921  isnumbasabl  38178  isnumbasgrp  38179  dfacbasgrp  38180  trclimalb2  38520  frege81d  38541  fnfvimad  39958  fnfvima2  39977  imass2d  39979  limccog  40355  liminfgord  40489
  Copyright terms: Public domain W3C validator