Theorem imass2 6055

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

Step	Hyp	Ref	Expression
1		ssres2 5957	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵))
2		rnss 5883	. . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵))
4		df-ima 5632	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
5		df-ima 5632	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
6	3, 4, 5	3sstr4g 3984	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵))

Syntax hints:   → wi 4   ⊆ wss 3898  ran crn 5620   ↾ cres 5621   “ cima 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  funimass1  6568  funimass2  6569  fvimacnv  6992  fnfvimad  7174  f1imass  7204  ecinxp  8722  sbthlem1  9007  sbthlem2  9008  php3  9125  ordtypelem2  9412  tcrank  9784  limsupgord  15381  isercoll  15577  isacs1i  17565  gsumzf1o  19826  dprdres  19944  dprd2da  19958  dmdprdsplit2lem  19961  lmhmlsp  20985  f1lindf  21761  iscnp4  23179  cnpco  23183  cncls2i  23186  cnntri  23187  cnrest2  23202  cnpresti  23204  cnprest  23205  1stcfb  23361  xkococnlem  23575  qtopval2  23612  tgqtop  23628  qtoprest  23633  kqdisj  23648  regr1lem  23655  kqreglem1  23657  kqreglem2  23658  kqnrmlem1  23659  kqnrmlem2  23660  nrmhmph  23710  fbasrn  23800  elfm2  23864  fmfnfmlem1  23870  fmco  23877  flffbas  23911  cnpflf2  23916  cnextcn  23983  metcnp3  24456  metustto  24469  cfilucfil  24475  uniioombllem3  25514  dyadmbllem  25528  mbfconstlem  25556  i1fima2  25608  itg2gt0  25689  ellimc3  25808  limcflf  25810  limcresi  25814  limciun  25823  lhop  25949  ig1peu  26108  ig1pdvds  26113  psercnlem2  26362  dvloglem  26585  efopn  26595  noetalem1  27681  madess  27822  oldss  27824  cofcut1  27865  negsproplem2  27972  bdayon  28210  fnpreimac  32655  fsuppinisegfi  32672  gsumpart  33044  elrgspnsubrunlem2  33222  txomap  33868  zarcmplem  33915  tpr2rico  33946  pthhashvtx  35193  cvmsss2  35339  cvmopnlem  35343  cvmliftmolem1  35346  cvmliftlem15  35363  cvmlift2lem9  35376  imadifss  37655  poimirlem1  37681  poimirlem2  37682  poimirlem3  37683  poimirlem15  37695  poimirlem30  37710  dvtan  37730  heibor1lem  37869  aks6d1c2  42243  aks6d1c6lem3  42285  aks6d1c6lem5  42290  isnumbasabl  43223  isnumbasgrp  43224  dfacbasgrp  43225  trclimalb2  43843  frege81d  43864  imass2d  45382  limccog  45744  liminfgord  45876  uhgrimisgrgriclem  48054  clnbgrgrim  48058