Theorem imass2 6057

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

Syntax hints:   → wi 4   ⊆ wss 3905  ran crn 5624   ↾ cres 5625   “ cima 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636

This theorem is referenced by:  funimass1  6568  funimass2  6569  fvimacnv  6991  fnfvimad  7174  f1imass  7205  ecinxp  8726  sbthlem1  9011  sbthlem2  9012  php3  9133  ordtypelem2  9430  tcrank  9799  limsupgord  15397  isercoll  15593  isacs1i  17581  gsumzf1o  19809  dprdres  19927  dprd2da  19941  dmdprdsplit2lem  19944  lmhmlsp  20971  f1lindf  21747  iscnp4  23166  cnpco  23170  cncls2i  23173  cnntri  23174  cnrest2  23189  cnpresti  23191  cnprest  23192  1stcfb  23348  xkococnlem  23562  qtopval2  23599  tgqtop  23615  qtoprest  23620  kqdisj  23635  regr1lem  23642  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  nrmhmph  23697  fbasrn  23787  elfm2  23851  fmfnfmlem1  23857  fmco  23864  flffbas  23898  cnpflf2  23903  cnextcn  23970  metcnp3  24444  metustto  24457  cfilucfil  24463  uniioombllem3  25502  dyadmbllem  25516  mbfconstlem  25544  i1fima2  25596  itg2gt0  25677  ellimc3  25796  limcflf  25798  limcresi  25802  limciun  25811  lhop  25937  ig1peu  26096  ig1pdvds  26101  psercnlem2  26350  dvloglem  26573  efopn  26583  noetalem1  27669  madess  27808  oldss  27810  cofcut1  27851  negsproplem2  27958  bdayon  28196  fnpreimac  32628  fsuppinisegfi  32643  gsumpart  33023  elrgspnsubrunlem2  33198  txomap  33800  zarcmplem  33847  tpr2rico  33878  pthhashvtx  35100  cvmsss2  35246  cvmopnlem  35250  cvmliftmolem1  35253  cvmliftlem15  35270  cvmlift2lem9  35283  imadifss  37574  poimirlem1  37600  poimirlem2  37601  poimirlem3  37602  poimirlem15  37614  poimirlem30  37629  dvtan  37649  heibor1lem  37788  aks6d1c2  42103  aks6d1c6lem3  42145  aks6d1c6lem5  42150  isnumbasabl  43079  isnumbasgrp  43080  dfacbasgrp  43081  trclimalb2  43699  frege81d  43720  imass2d  45239  limccog  45602  liminfgord  45736  uhgrimisgrgriclem  47915  clnbgrgrim  47919