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

Theorem imass2 6059
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 5970 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 rnss 5899 . . 3 ((𝐶𝐴) ⊆ (𝐶𝐵) → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
31, 2syl 17 . 2 (𝐴𝐵 → ran (𝐶𝐴) ⊆ ran (𝐶𝐵))
4 df-ima 5651 . 2 (𝐶𝐴) = ran (𝐶𝐴)
5 df-ima 5651 . 2 (𝐶𝐵) = ran (𝐶𝐵)
63, 4, 53sstr4g 3994 1 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3915  ran crn 5639  cres 5640  cima 5641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651
This theorem is referenced by:  funimass1  6588  funimass2  6589  fvimacnv  7008  fnfvimad  7189  f1imass  7216  ecinxp  8738  sbthlem1  9034  sbthlem2  9035  php3  9163  php3OLD  9175  ordtypelem2  9462  tcrank  9827  limsupgord  15361  isercoll  15559  isacs1i  17544  gsumzf1o  19696  dprdres  19814  dprd2da  19828  dmdprdsplit2lem  19831  lmhmlsp  20526  f1lindf  21244  iscnp4  22630  cnpco  22634  cncls2i  22637  cnntri  22638  cnrest2  22653  cnpresti  22655  cnprest  22656  1stcfb  22812  xkococnlem  23026  qtopval2  23063  tgqtop  23079  qtoprest  23084  kqdisj  23099  regr1lem  23106  kqreglem1  23108  kqreglem2  23109  kqnrmlem1  23110  kqnrmlem2  23111  nrmhmph  23161  fbasrn  23251  elfm2  23315  fmfnfmlem1  23321  fmco  23328  flffbas  23362  cnpflf2  23367  cnextcn  23434  metcnp3  23912  metustto  23925  cfilucfil  23931  uniioombllem3  24965  dyadmbllem  24979  mbfconstlem  25007  i1fima2  25059  itg2gt0  25141  ellimc3  25259  limcflf  25261  limcresi  25265  limciun  25274  lhop  25396  ig1peu  25552  ig1pdvds  25557  psercnlem2  25799  dvloglem  26019  efopn  26029  noetalem1  27105  madess  27228  cofcut1  27261  negsproplem2  27349  fnpreimac  31629  fsuppinisegfi  31644  gsumpart  31939  txomap  32455  zarcmplem  32502  tpr2rico  32533  pthhashvtx  33761  cvmsss2  33908  cvmopnlem  33912  cvmliftmolem1  33915  cvmliftlem15  33932  cvmlift2lem9  33945  imadifss  36082  poimirlem1  36108  poimirlem2  36109  poimirlem3  36110  poimirlem15  36122  poimirlem30  36137  dvtan  36157  heibor1lem  36297  isnumbasabl  41462  isnumbasgrp  41463  dfacbasgrp  41464  trclimalb2  42072  frege81d  42093  imass2d  43564  limccog  43935  liminfgord  44069
  Copyright terms: Public domain W3C validator