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

Theorem imass2 5943
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 5859 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 rnss 5786 . . 3 ((𝐶𝐴) ⊆ (𝐶𝐵) → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
31, 2syl 17 . 2 (𝐴𝐵 → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
4 df-ima 5545 . 2 (𝐶𝐴) = ran (𝐶𝐴)
5 df-ima 5545 . 2 (𝐶𝐵) = ran (𝐶𝐵)
63, 4, 53sstr4g 3987 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3908  ran crn 5533  cres 5534  cima 5535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-rab 3139  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-br 5043  df-opab 5105  df-xp 5538  df-cnv 5540  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545
This theorem is referenced by:  funimass1  6415  funimass2  6416  fvimacnv  6805  fnfvimad  6979  f1imass  7005  ecinxp  8359  sbthlem1  8615  sbthlem2  8616  php3  8691  ordtypelem2  8971  tcrank  9301  limsupgord  14820  isercoll  15015  isacs1i  16919  gsumzf1o  19023  dprdres  19141  dprd2da  19155  dmdprdsplit2lem  19158  lmhmlsp  19812  f1lindf  20509  iscnp4  21866  cnpco  21870  cncls2i  21873  cnntri  21874  cnrest2  21889  cnpresti  21891  cnprest  21892  1stcfb  22048  xkococnlem  22262  qtopval2  22299  tgqtop  22315  qtoprest  22320  kqdisj  22335  regr1lem  22342  kqreglem1  22344  kqreglem2  22345  kqnrmlem1  22346  kqnrmlem2  22347  nrmhmph  22397  fbasrn  22487  elfm2  22551  fmfnfmlem1  22557  fmco  22564  flffbas  22598  cnpflf2  22603  cnextcn  22670  metcnp3  23145  metustto  23158  cfilucfil  23164  uniioombllem3  24187  dyadmbllem  24201  mbfconstlem  24229  i1fima2  24281  itg2gt0  24362  ellimc3  24480  limcflf  24482  limcresi  24486  limciun  24495  lhop  24617  ig1peu  24770  ig1pdvds  24775  psercnlem2  25017  dvloglem  25237  efopn  25247  fnpreimac  30424  txomap  31156  tpr2rico  31229  pthhashvtx  32448  cvmsss2  32595  cvmopnlem  32599  cvmliftmolem1  32602  cvmliftlem15  32619  cvmlift2lem9  32632  imadifss  34990  poimirlem1  35016  poimirlem2  35017  poimirlem3  35018  poimirlem15  35030  poimirlem30  35045  dvtan  35065  heibor1lem  35205  isnumbasabl  39980  isnumbasgrp  39981  dfacbasgrp  39982  trclimalb2  40357  frege81d  40378  imass2d  41840  limccog  42201  liminfgord  42335
  Copyright terms: Public domain W3C validator