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

Theorem imass2 5403
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 5328 . . 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-xp 5030  df-cnv 5032  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037
This theorem is referenced by:  funimass1  5867  funimass2  5868  fvimacnv  6221  f1imass  6396  ecinxp  7682  sbthlem1  7928  sbthlem2  7929  php3  8004  ordtypelem2  8280  tcrank  8603  limsupgord  13993  isercoll  14188  isacs1i  16083  gsumzf1o  18078  dprdres  18192  dprd2da  18206  dmdprdsplit2lem  18209  lmhmlsp  18812  f1lindf  19918  iscnp4  20815  cnpco  20819  cncls2i  20822  cnntri  20823  cnrest2  20838  cnpresti  20840  cnprest  20841  1stcfb  20996  xkococnlem  21210  qtopval2  21247  tgqtop  21263  qtoprest  21268  kqdisj  21283  regr1lem  21290  kqreglem1  21292  kqreglem2  21293  kqnrmlem1  21294  kqnrmlem2  21295  nrmhmph  21345  fbasrn  21436  elfm2  21500  fmfnfmlem1  21506  fmco  21513  flffbas  21547  cnpflf2  21552  cnextcn  21619  metcnp3  22092  metustto  22105  cfilucfil  22111  uniioombllem3  23072  dyadmbllem  23086  mbfconstlem  23115  i1fima2  23165  itg2gt0  23246  ellimc3  23362  limcflf  23364  limcresi  23368  limciun  23377  lhop  23496  ig1peu  23648  ig1pdvds  23653  psercnlem2  23895  dvloglem  24107  efopn  24117  txomap  29031  tpr2rico  29088  cvmsss2  30312  cvmopnlem  30316  cvmliftmolem1  30319  cvmliftlem15  30336  cvmlift2lem9  30349  nofulllem3  30905  imadifss  32353  poimirlem1  32379  poimirlem2  32380  poimirlem3  32381  poimirlem15  32393  poimirlem30  32408  dvtan  32429  heibor1lem  32577  isnumbasabl  36494  isnumbasgrp  36495  dfacbasgrp  36496  trclimalb2  36836  frege81d  36857  limccog  38487
  Copyright terms: Public domain W3C validator