Theorem imass2 5501

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

Syntax hints:   → wi 4   ⊆ wss 3574  ran crn 5115   ↾ cres 5116   “ cima 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  funimass1  5971  funimass2  5972  fvimacnv  6332  f1imass  6521  ecinxp  7822  sbthlem1  8070  sbthlem2  8071  php3  8146  ordtypelem2  8424  tcrank  8747  limsupgord  14203  isercoll  14398  isacs1i  16318  gsumzf1o  18313  dprdres  18427  dprd2da  18441  dmdprdsplit2lem  18444  lmhmlsp  19049  f1lindf  20161  iscnp4  21067  cnpco  21071  cncls2i  21074  cnntri  21075  cnrest2  21090  cnpresti  21092  cnprest  21093  1stcfb  21248  xkococnlem  21462  qtopval2  21499  tgqtop  21515  qtoprest  21520  kqdisj  21535  regr1lem  21542  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  nrmhmph  21597  fbasrn  21688  elfm2  21752  fmfnfmlem1  21758  fmco  21765  flffbas  21799  cnpflf2  21804  cnextcn  21871  metcnp3  22345  metustto  22358  cfilucfil  22364  uniioombllem3  23353  dyadmbllem  23367  mbfconstlem  23396  i1fima2  23446  itg2gt0  23527  ellimc3  23643  limcflf  23645  limcresi  23649  limciun  23658  lhop  23779  ig1peu  23931  ig1pdvds  23936  psercnlem2  24178  dvloglem  24394  efopn  24404  txomap  29901  tpr2rico  29958  cvmsss2  31256  cvmopnlem  31260  cvmliftmolem1  31263  cvmliftlem15  31280  cvmlift2lem9  31293  imadifss  33384  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem15  33424  poimirlem30  33439  dvtan  33460  heibor1lem  33608  isnumbasabl  37676  isnumbasgrp  37677  dfacbasgrp  37678  trclimalb2  38018  frege81d  38039  fnfvimad  39459  fnfvima2  39478  imass2d  39480  limccog  39852  liminfgord  39986