Theorem imass2 6106

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 6005	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵))
2		rnss 5931	. . 3 ⊢ ((𝐶 ↾ 𝐴) ⊆ (𝐶 ↾ 𝐵) → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵))
3	1, 2	syl 18	. 2 ⊢ (𝐴 ⊆ 𝐵 → ran (𝐶 ↾ 𝐴) ⊆ ran (𝐶 ↾ 𝐵))
4		df-ima 5676	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
5		df-ima 5676	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
6	3, 4, 5	3sstr4g 3991	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵))

Syntax hints:   → wi 4   ⊆ wss 3906  ran crn 5664   ↾ cres 5665   “ cima 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is referenced by:  funimass1  6620  funimass2  6621  fvimacnv  7050  fnfvimad  7234  f1imass  7264  ecinxp  8791  sbthlem1  9076  sbthlem2  9077  php3  9194  ordtypelem2  9482  tcrank  9857  limsupgord  15525  isercoll  15721  isacs1i  17714  gsumzf1o  19983  dprdres  20101  dprd2da  20115  dmdprdsplit2lem  20118  lmhmlsp  21151  f1lindf  21953  iscnp4  23401  cnpco  23405  cncls2i  23408  cnntri  23409  cnrest2  23424  cnpresti  23426  cnprest  23427  1stcfb  23583  xkococnlem  23797  qtopval2  23834  tgqtop  23850  qtoprest  23855  kqdisj  23870  regr1lem  23877  kqreglem1  23879  kqreglem2  23880  kqnrmlem1  23881  kqnrmlem2  23882  nrmhmph  23932  fbasrn  24022  elfm2  24086  fmfnfmlem1  24092  fmco  24099  flffbas  24133  cnpflf2  24138  cnextcn  24205  metcnp3  24678  metustto  24691  cfilucfil  24697  uniioombllem3  25725  dyadmbllem  25739  mbfconstlem  25767  i1fima2  25819  itg2gt0  25900  ellimc3  26019  limcflf  26021  limcresi  26025  limciun  26034  lhop  26156  ig1peu  26313  ig1pdvds  26318  psercnlem2  26565  dvloglem  26791  efopn  26801  noetalem1  27883  madess  28037  oldss  28041  cofcut1  28091  negsproplem2  28200  bdayons  28447  fnpreimac  32993  fsuppinisegfi  33010  gsumpart  33361  elrgspnsubrunlem2  33546  txomap  34202  zarcmplem  34249  tpr2rico  34280  pthhashvtx  35598  cvmsss2  35744  cvmopnlem  35748  cvmliftmolem1  35751  cvmliftlem15  35768  cvmlift2lem9  35781  imadifss  38224  poimirlem1  38250  poimirlem2  38251  poimirlem3  38252  poimirlem15  38264  poimirlem30  38279  dvtan  38299  heibor1lem  38438  aks6d1c2  42875  aks6d1c6lem3  42917  aks6d1c6lem5  42922  isnumbasabl  43813  isnumbasgrp  43814  dfacbasgrp  43815  trclimalb2  44432  frege81d  44453  imass2d  45956  limccog  46316  liminfgord  46448  uhgrimisgrgriclem  48672  clnbgrgrim  48676