Theorem imass2 6096

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ran crn 5652   ↾ cres 5653   “ cima 5654

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  funimass1  6614  funimass2  6615  fvimacnv  7044  fnfvimad  7232  f1imass  7260  ecinxp  8797  sbthlem1  9090  sbthlem2  9091  php3  9208  ordtypelem2  9497  tcrank  9882  limsupgord  15619  isercoll  15815  isacs1i  17811  gsumzf1o  20106  dprdres  20224  dprd2da  20238  dmdprdsplit2lem  20241  lmhmlsp  21304  f1lindf  22108  iscnp4  23561  cnpco  23565  cncls2i  23568  cnntri  23569  cnrest2  23584  cnpresti  23586  cnprest  23587  1stcfb  23743  xkococnlem  23958  qtopval2  23995  tgqtop  24011  qtoprest  24016  kqdisj  24031  regr1lem  24038  kqreglem1  24040  kqreglem2  24041  kqnrmlem1  24042  kqnrmlem2  24043  nrmhmph  24093  fbasrn  24183  elfm2  24247  fmfnfmlem1  24253  fmco  24260  flffbas  24294  cnpflf2  24299  cnextcn  24366  metcnp3  24839  metustto  24852  cfilucfil  24858  uniioombllem3  25886  dyadmbllem  25900  mbfconstlem  25928  i1fima2  25980  itg2gt0  26061  ellimc3  26179  limcflf  26181  limcresi  26185  limciun  26194  lhop  26316  ig1peu  26473  ig1pdvds  26478  psercnlem2  26733  dvloglem  26958  efopn  26968  noetalem1  28080  madess  28234  oldss  28238  cofcut1  28288  negsproplem2  28397  bdayons  28644  pthhashvtx  30297  fnpreimac  33246  fsuppinisegfi  33262  gsumpart  33606  elrgspnsubrunlem2  33791  txomap  34448  zarcmplem  34495  tpr2rico  34526  cvmsss2  36008  cvmopnlem  36012  cvmliftmolem1  36015  cvmliftlem15  36032  cvmlift2lem9  36045  imadifss  38491  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem15  38521  poimirlem30  38536  dvtan  38556  heibor1lem  38711  aks6d1c2  43148  aks6d1c6lem3  43190  aks6d1c6lem5  43195  isnumbasabl  44066  isnumbasgrp  44067  dfacbasgrp  44068  trclimalb2  44685  frege81d  44706  imass2d  46216  limccog  46576  liminfgord  46708  uhgrimisgrgriclem  48972  clnbgrgrim  48976