Theorem imass2 6054

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895  ran crn 5651   ↾ cres 5652   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  imassrn  6197  funimass1  6622  funimass2  6623  fvimacnv  7052  fnfvimad  7240  f1imass  7268  ecinxp  8816  sbthlem1  9109  sbthlem2  9110  php3  9227  ordtypelem2  9516  tcrank  9904  limsupgord  15644  isercoll  15840  isacs1i  17836  gsumzf1o  20131  dprdres  20249  dprd2da  20263  dmdprdsplit2lem  20266  lmhmlsp  21329  f1lindf  22133  iscnp4  23586  cnpco  23590  cncls2i  23593  cnntri  23594  cnrest2  23609  cnpresti  23611  cnprest  23612  1stcfb  23768  xkococnlem  23983  qtopval2  24020  tgqtop  24036  qtoprest  24041  kqdisj  24056  regr1lem  24063  kqreglem1  24065  kqreglem2  24066  kqnrmlem1  24067  kqnrmlem2  24068  nrmhmph  24118  fbasrn  24208  elfm2  24272  fmfnfmlem1  24278  fmco  24285  flffbas  24319  cnpflf2  24324  cnextcn  24391  metcnp3  24864  metustto  24877  cfilucfil  24883  uniioombllem3  25911  dyadmbllem  25925  mbfconstlem  25953  i1fima2  26005  itg2gt0  26086  ellimc3  26204  limcflf  26206  limcresi  26210  limciun  26219  lhop  26341  ig1peu  26498  ig1pdvds  26503  psercnlem2  26756  dvloglem  26981  efopn  26991  noetalem1  28103  madess  28257  oldss  28261  cofcut1  28311  negsproplem2  28420  bdayons  28667  pthhashvtx  30320  fnpreimac  33311  fsuppinisegfi  33327  gsumpart  33670  elrgspnsubrunlem2  33855  txomap  34512  zarcmplem  34559  tpr2rico  34590  cvmsss2  36125  cvmopnlem  36129  cvmliftmolem1  36132  cvmliftlem15  36149  cvmlift2lem9  36162  imadifss  38616  poimirlem1  38632  poimirlem2  38633  poimirlem3  38634  poimirlem15  38646  poimirlem30  38661  dvtan  38681  heibor1lem  38836  aks6d1c2  43273  aks6d1c6lem3  43315  aks6d1c6lem5  43320  isnumbasabl  44201  isnumbasgrp  44202  dfacbasgrp  44203  trclimalb2  44819  frege81d  44840  imass2d  46366  limccog  46725  liminfgord  46857  uhgrimisgrgriclem  49121  clnbgrgrim  49125