Theorem imass2 5959

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

Syntax hints:   → wi 4   ⊆ wss 3935  ran crn 5550   ↾ cres 5551   “ cima 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-br 5059  df-opab 5121  df-xp 5555  df-cnv 5557  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562

This theorem is referenced by:  funimass1  6430  funimass2  6431  fvimacnv  6817  fnfvimad  6990  f1imass  7016  ecinxp  8366  sbthlem1  8621  sbthlem2  8622  php3  8697  ordtypelem2  8977  tcrank  9307  limsupgord  14823  isercoll  15018  isacs1i  16922  gsumzf1o  19026  dprdres  19144  dprd2da  19158  dmdprdsplit2lem  19161  lmhmlsp  19815  f1lindf  20960  iscnp4  21865  cnpco  21869  cncls2i  21872  cnntri  21873  cnrest2  21888  cnpresti  21890  cnprest  21891  1stcfb  22047  xkococnlem  22261  qtopval2  22298  tgqtop  22314  qtoprest  22319  kqdisj  22334  regr1lem  22341  kqreglem1  22343  kqreglem2  22344  kqnrmlem1  22345  kqnrmlem2  22346  nrmhmph  22396  fbasrn  22486  elfm2  22550  fmfnfmlem1  22556  fmco  22563  flffbas  22597  cnpflf2  22602  cnextcn  22669  metcnp3  23144  metustto  23157  cfilucfil  23163  uniioombllem3  24180  dyadmbllem  24194  mbfconstlem  24222  i1fima2  24274  itg2gt0  24355  ellimc3  24471  limcflf  24473  limcresi  24477  limciun  24486  lhop  24607  ig1peu  24759  ig1pdvds  24764  psercnlem2  25006  dvloglem  25225  efopn  25235  fnpreimac  30410  txomap  31093  tpr2rico  31150  pthhashvtx  32369  cvmsss2  32516  cvmopnlem  32520  cvmliftmolem1  32523  cvmliftlem15  32540  cvmlift2lem9  32553  imadifss  34861  poimirlem1  34887  poimirlem2  34888  poimirlem3  34889  poimirlem15  34901  poimirlem30  34916  dvtan  34936  heibor1lem  35081  isnumbasabl  39699  isnumbasgrp  39700  dfacbasgrp  39701  trclimalb2  40064  frege81d  40085  imass2d  41529  limccog  41894  liminfgord  42028