Theorem imass2 6102

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902  ran crn 5660   ↾ cres 5661   “ cima 5662

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is used by:  funimass1  6619  funimass2  6620  fvimacnv  7049  fnfvimad  7237  f1imass  7265  ecinxp  8796  sbthlem1  9089  sbthlem2  9090  php3  9207  ordtypelem2  9495  tcrank  9870  limsupgord  15563  isercoll  15759  isacs1i  17751  gsumzf1o  20045  dprdres  20163  dprd2da  20177  dmdprdsplit2lem  20180  lmhmlsp  21239  f1lindf  22041  iscnp4  23494  cnpco  23498  cncls2i  23501  cnntri  23502  cnrest2  23517  cnpresti  23519  cnprest  23520  1stcfb  23676  xkococnlem  23891  qtopval2  23928  tgqtop  23944  qtoprest  23949  kqdisj  23964  regr1lem  23971  kqreglem1  23973  kqreglem2  23974  kqnrmlem1  23975  kqnrmlem2  23976  nrmhmph  24026  fbasrn  24116  elfm2  24180  fmfnfmlem1  24186  fmco  24193  flffbas  24227  cnpflf2  24232  cnextcn  24299  metcnp3  24772  metustto  24785  cfilucfil  24791  uniioombllem3  25819  dyadmbllem  25833  mbfconstlem  25861  i1fima2  25913  itg2gt0  25994  ellimc3  26113  limcflf  26115  limcresi  26119  limciun  26128  lhop  26250  ig1peu  26407  ig1pdvds  26412  psercnlem2  26667  dvloglem  26893  efopn  26903  noetalem1  27985  madess  28139  oldss  28143  cofcut1  28193  negsproplem2  28302  bdayons  28549  pthhashvtx  30202  fnpreimac  33151  fsuppinisegfi  33167  gsumpart  33511  elrgspnsubrunlem2  33696  txomap  34352  zarcmplem  34399  tpr2rico  34430  cvmsss2  35861  cvmopnlem  35865  cvmliftmolem1  35868  cvmliftlem15  35885  cvmlift2lem9  35898  imadifss  38362  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem15  38392  poimirlem30  38407  dvtan  38427  heibor1lem  38567  aks6d1c2  43004  aks6d1c6lem3  43046  aks6d1c6lem5  43051  isnumbasabl  43955  isnumbasgrp  43956  dfacbasgrp  43957  trclimalb2  44574  frege81d  44595  imass2d  46098  limccog  46458  liminfgord  46590  uhgrimisgrgriclem  48854  clnbgrgrim  48858