Theorem imass2 6076

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

Syntax hints:   → wi 4   ⊆ wss 3917  ran crn 5642   ↾ cres 5643   “ cima 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  funimass1  6601  funimass2  6602  fvimacnv  7028  fnfvimad  7211  f1imass  7242  ecinxp  8768  sbthlem1  9057  sbthlem2  9058  php3  9179  ordtypelem2  9479  tcrank  9844  limsupgord  15445  isercoll  15641  isacs1i  17625  gsumzf1o  19849  dprdres  19967  dprd2da  19981  dmdprdsplit2lem  19984  lmhmlsp  20963  f1lindf  21738  iscnp4  23157  cnpco  23161  cncls2i  23164  cnntri  23165  cnrest2  23180  cnpresti  23182  cnprest  23183  1stcfb  23339  xkococnlem  23553  qtopval2  23590  tgqtop  23606  qtoprest  23611  kqdisj  23626  regr1lem  23633  kqreglem1  23635  kqreglem2  23636  kqnrmlem1  23637  kqnrmlem2  23638  nrmhmph  23688  fbasrn  23778  elfm2  23842  fmfnfmlem1  23848  fmco  23855  flffbas  23889  cnpflf2  23894  cnextcn  23961  metcnp3  24435  metustto  24448  cfilucfil  24454  uniioombllem3  25493  dyadmbllem  25507  mbfconstlem  25535  i1fima2  25587  itg2gt0  25668  ellimc3  25787  limcflf  25789  limcresi  25793  limciun  25802  lhop  25928  ig1peu  26087  ig1pdvds  26092  psercnlem2  26341  dvloglem  26564  efopn  26574  noetalem1  27660  madess  27795  cofcut1  27835  negsproplem2  27942  bdayon  28180  fnpreimac  32602  fsuppinisegfi  32617  gsumpart  33004  elrgspnsubrunlem2  33206  txomap  33831  zarcmplem  33878  tpr2rico  33909  pthhashvtx  35122  cvmsss2  35268  cvmopnlem  35272  cvmliftmolem1  35275  cvmliftlem15  35292  cvmlift2lem9  35305  imadifss  37596  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem15  37636  poimirlem30  37651  dvtan  37671  heibor1lem  37810  aks6d1c2  42125  aks6d1c6lem3  42167  aks6d1c6lem5  42172  isnumbasabl  43102  isnumbasgrp  43103  dfacbasgrp  43104  trclimalb2  43722  frege81d  43743  imass2d  45262  limccog  45625  liminfgord  45759  uhgrimisgrgriclem  47934  clnbgrgrim  47938