Theorem imass2 6132

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

Syntax hints:   → wi 4   ⊆ wss 3976  ran crn 5701   ↾ cres 5702   “ cima 5703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713

This theorem is referenced by:  funimass1  6660  funimass2  6661  fvimacnv  7086  fnfvimad  7271  f1imass  7301  ecinxp  8850  sbthlem1  9149  sbthlem2  9150  php3  9275  php3OLD  9287  ordtypelem2  9588  tcrank  9953  limsupgord  15518  isercoll  15716  isacs1i  17715  gsumzf1o  19954  dprdres  20072  dprd2da  20086  dmdprdsplit2lem  20089  lmhmlsp  21071  f1lindf  21865  iscnp4  23292  cnpco  23296  cncls2i  23299  cnntri  23300  cnrest2  23315  cnpresti  23317  cnprest  23318  1stcfb  23474  xkococnlem  23688  qtopval2  23725  tgqtop  23741  qtoprest  23746  kqdisj  23761  regr1lem  23768  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  nrmhmph  23823  fbasrn  23913  elfm2  23977  fmfnfmlem1  23983  fmco  23990  flffbas  24024  cnpflf2  24029  cnextcn  24096  metcnp3  24574  metustto  24587  cfilucfil  24593  uniioombllem3  25639  dyadmbllem  25653  mbfconstlem  25681  i1fima2  25733  itg2gt0  25815  ellimc3  25934  limcflf  25936  limcresi  25940  limciun  25949  lhop  26075  ig1peu  26234  ig1pdvds  26239  psercnlem2  26486  dvloglem  26708  efopn  26718  noetalem1  27804  madess  27933  cofcut1  27972  negsproplem2  28079  fnpreimac  32689  fsuppinisegfi  32699  gsumpart  33038  txomap  33780  zarcmplem  33827  tpr2rico  33858  pthhashvtx  35095  cvmsss2  35242  cvmopnlem  35246  cvmliftmolem1  35249  cvmliftlem15  35266  cvmlift2lem9  35279  imadifss  37555  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem15  37595  poimirlem30  37610  dvtan  37630  heibor1lem  37769  aks6d1c2  42087  aks6d1c6lem3  42129  aks6d1c6lem5  42134  isnumbasabl  43063  isnumbasgrp  43064  dfacbasgrp  43065  trclimalb2  43688  frege81d  43709  imass2d  45171  limccog  45541  liminfgord  45675  uhgrimisgrgriclem  47782  clnbgrgrim  47786