Theorem imass2 6109

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908  ran crn 5667   ↾ cres 5668   “ cima 5669

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-cnv 5674  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679

This theorem is used by:  funimass1  6625  funimass2  6626  fvimacnv  7055  fnfvimad  7239  f1imass  7269  ecinxp  8799  sbthlem1  9085  sbthlem2  9086  php3  9203  ordtypelem2  9491  tcrank  9866  limsupgord  15549  isercoll  15745  isacs1i  17738  gsumzf1o  20013  dprdres  20131  dprd2da  20145  dmdprdsplit2lem  20148  lmhmlsp  21207  f1lindf  22009  iscnp4  23457  cnpco  23461  cncls2i  23464  cnntri  23465  cnrest2  23480  cnpresti  23482  cnprest  23483  1stcfb  23639  xkococnlem  23853  qtopval2  23890  tgqtop  23906  qtoprest  23911  kqdisj  23926  regr1lem  23933  kqreglem1  23935  kqreglem2  23936  kqnrmlem1  23937  kqnrmlem2  23938  nrmhmph  23988  fbasrn  24078  elfm2  24142  fmfnfmlem1  24148  fmco  24155  flffbas  24189  cnpflf2  24194  cnextcn  24261  metcnp3  24734  metustto  24747  cfilucfil  24753  uniioombllem3  25781  dyadmbllem  25795  mbfconstlem  25823  i1fima2  25875  itg2gt0  25956  ellimc3  26075  limcflf  26077  limcresi  26081  limciun  26090  lhop  26212  ig1peu  26369  ig1pdvds  26374  psercnlem2  26624  dvloglem  26850  efopn  26860  noetalem1  27942  madess  28096  oldss  28100  cofcut1  28150  negsproplem2  28259  bdayons  28506  fnpreimac  33052  fsuppinisegfi  33069  gsumpart  33414  elrgspnsubrunlem2  33599  txomap  34255  zarcmplem  34302  tpr2rico  34333  pthhashvtx  35641  cvmsss2  35787  cvmopnlem  35791  cvmliftmolem1  35794  cvmliftlem15  35811  cvmlift2lem9  35824  imadifss  38287  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem15  38327  poimirlem30  38342  dvtan  38362  heibor1lem  38501  aks6d1c2  42938  aks6d1c6lem3  42980  aks6d1c6lem5  42985  isnumbasabl  43874  isnumbasgrp  43875  dfacbasgrp  43876  trclimalb2  44493  frege81d  44514  imass2d  46017  limccog  46377  liminfgord  46509  uhgrimisgrgriclem  48736  clnbgrgrim  48740