Theorem imass2 5965

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

Syntax hints:   → wi 4   ⊆ wss 3936  ran crn 5556   ↾ cres 5557   “ cima 5558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568

This theorem is referenced by:  funimass1  6436  funimass2  6437  fvimacnv  6823  fnfvimad  6996  f1imass  7022  ecinxp  8372  sbthlem1  8627  sbthlem2  8628  php3  8703  ordtypelem2  8983  tcrank  9313  limsupgord  14829  isercoll  15024  isacs1i  16928  gsumzf1o  19032  dprdres  19150  dprd2da  19164  dmdprdsplit2lem  19167  lmhmlsp  19821  f1lindf  20966  iscnp4  21871  cnpco  21875  cncls2i  21878  cnntri  21879  cnrest2  21894  cnpresti  21896  cnprest  21897  1stcfb  22053  xkococnlem  22267  qtopval2  22304  tgqtop  22320  qtoprest  22325  kqdisj  22340  regr1lem  22347  kqreglem1  22349  kqreglem2  22350  kqnrmlem1  22351  kqnrmlem2  22352  nrmhmph  22402  fbasrn  22492  elfm2  22556  fmfnfmlem1  22562  fmco  22569  flffbas  22603  cnpflf2  22608  cnextcn  22675  metcnp3  23150  metustto  23163  cfilucfil  23169  uniioombllem3  24186  dyadmbllem  24200  mbfconstlem  24228  i1fima2  24280  itg2gt0  24361  ellimc3  24477  limcflf  24479  limcresi  24483  limciun  24492  lhop  24613  ig1peu  24765  ig1pdvds  24770  psercnlem2  25012  dvloglem  25231  efopn  25241  fnpreimac  30416  txomap  31098  tpr2rico  31155  pthhashvtx  32374  cvmsss2  32521  cvmopnlem  32525  cvmliftmolem1  32528  cvmliftlem15  32545  cvmlift2lem9  32558  imadifss  34882  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem15  34922  poimirlem30  34937  dvtan  34957  heibor1lem  35102  isnumbasabl  39726  isnumbasgrp  39727  dfacbasgrp  39728  trclimalb2  40091  frege81d  40112  imass2d  41556  limccog  41921  liminfgord  42055