Theorem imass2 6067

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  ran crn 5656   ↾ cres 5657   “ cima 5658

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  imassrn  6210  funimass1  6644  funimass2  6645  fvimacnv  7075  fnfvimad  7263  f1imass  7291  ecinxp  8841  sbthlem1  9134  sbthlem2  9135  php3  9252  ordtypelem2  9540  tcrank  9928  limsupgord  15668  isercoll  15864  isacs1i  17860  gsumzf1o  20156  dprdres  20274  dprd2da  20288  dmdprdsplit2lem  20291  lmhmlsp  21354  f1lindf  22158  iscnp4  23611  cnpco  23615  cncls2i  23618  cnntri  23619  cnrest2  23634  cnpresti  23636  cnprest  23637  1stcfb  23793  xkococnlem  24008  qtopval2  24045  tgqtop  24061  qtoprest  24066  kqdisj  24081  regr1lem  24088  kqreglem1  24090  kqreglem2  24091  kqnrmlem1  24092  kqnrmlem2  24093  nrmhmph  24143  fbasrn  24233  elfm2  24297  fmfnfmlem1  24303  fmco  24310  flffbas  24344  cnpflf2  24349  cnextcn  24416  metcnp3  24889  metustto  24902  cfilucfil  24908  uniioombllem3  25936  dyadmbllem  25950  mbfconstlem  25978  i1fima2  26030  itg2gt0  26111  ellimc3  26229  limcflf  26231  limcresi  26235  limciun  26244  lhop  26366  ig1peu  26523  ig1pdvds  26528  psercnlem2  26781  dvloglem  27006  efopn  27016  noetalem1  28128  madess  28282  oldss  28286  cofcut1  28336  negsproplem2  28445  bdayons  28692  pthhashvtx  30345  fnpreimac  33336  fsuppinisegfi  33351  gsumpart  33694  elrgspnsubrunlem2  33879  txomap  34536  zarcmplem  34583  tpr2rico  34614  cvmsss2  36206  cvmopnlem  36210  cvmliftmolem1  36213  cvmliftlem15  36230  cvmlift2lem9  36243  imadifss  38715  poimirlem1  38731  poimirlem2  38732  poimirlem3  38733  poimirlem15  38745  poimirlem30  38760  dvtan  38780  heibor1lem  38935  aks6d1c2  43372  aks6d1c6lem3  43414  aks6d1c6lem5  43419  isnumbasabl  44300  isnumbasgrp  44301  dfacbasgrp  44302  trclimalb2  44918  frege81d  44939  imass2d  46478  limccog  46837  liminfgord  46969  uhgrimisgrgriclem  49233  clnbgrgrim  49237