Theorem imass2 6112

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

Syntax hints:   → wi 4   ⊆ wss 3947  ran crn 5683   ↾ cres 5684   “ cima 5685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5154  df-opab 5216  df-xp 5688  df-cnv 5690  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695

This theorem is referenced by:  funimass1  6641  funimass2  6642  fvimacnv  7066  fnfvimad  7251  f1imass  7279  ecinxp  8821  sbthlem1  9121  sbthlem2  9122  php3  9246  php3OLD  9258  ordtypelem2  9562  tcrank  9927  limsupgord  15474  isercoll  15672  isacs1i  17670  gsumzf1o  19910  dprdres  20028  dprd2da  20042  dmdprdsplit2lem  20045  lmhmlsp  21027  f1lindf  21820  iscnp4  23258  cnpco  23262  cncls2i  23265  cnntri  23266  cnrest2  23281  cnpresti  23283  cnprest  23284  1stcfb  23440  xkococnlem  23654  qtopval2  23691  tgqtop  23707  qtoprest  23712  kqdisj  23727  regr1lem  23734  kqreglem1  23736  kqreglem2  23737  kqnrmlem1  23738  kqnrmlem2  23739  nrmhmph  23789  fbasrn  23879  elfm2  23943  fmfnfmlem1  23949  fmco  23956  flffbas  23990  cnpflf2  23995  cnextcn  24062  metcnp3  24540  metustto  24553  cfilucfil  24559  uniioombllem3  25605  dyadmbllem  25619  mbfconstlem  25647  i1fima2  25699  itg2gt0  25781  ellimc3  25899  limcflf  25901  limcresi  25905  limciun  25914  lhop  26040  ig1peu  26202  ig1pdvds  26207  psercnlem2  26454  dvloglem  26675  efopn  26685  noetalem1  27771  madess  27900  cofcut1  27937  negsproplem2  28038  fnpreimac  32588  fsuppinisegfi  32599  gsumpart  32923  txomap  33649  zarcmplem  33696  tpr2rico  33727  pthhashvtx  34955  cvmsss2  35102  cvmopnlem  35106  cvmliftmolem1  35109  cvmliftlem15  35126  cvmlift2lem9  35139  imadifss  37296  poimirlem1  37322  poimirlem2  37323  poimirlem3  37324  poimirlem15  37336  poimirlem30  37351  dvtan  37371  heibor1lem  37510  aks6d1c2  41828  aks6d1c6lem3  41870  aks6d1c6lem5  41875  isnumbasabl  42767  isnumbasgrp  42768  dfacbasgrp  42769  trclimalb2  43393  frege81d  43414  imass2d  44871  limccog  45241  liminfgord  45375  uhgrimisgrgriclem  47477  clnbgrgrim  47481