Theorem imass2 6106

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

Syntax hints:   → wi 4   ⊆ wss 3947  ran crn 5679   ↾ cres 5680   “ cima 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-opab 5211  df-xp 5684  df-cnv 5686  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691

This theorem is referenced by:  funimass1  6635  funimass2  6636  fvimacnv  7062  fnfvimad  7246  f1imass  7274  ecinxp  8810  sbthlem1  9107  sbthlem2  9108  php3  9236  php3OLD  9248  ordtypelem2  9542  tcrank  9907  limsupgord  15448  isercoll  15646  isacs1i  17636  gsumzf1o  19866  dprdres  19984  dprd2da  19998  dmdprdsplit2lem  20001  lmhmlsp  20933  f1lindf  21755  iscnp4  23166  cnpco  23170  cncls2i  23173  cnntri  23174  cnrest2  23189  cnpresti  23191  cnprest  23192  1stcfb  23348  xkococnlem  23562  qtopval2  23599  tgqtop  23615  qtoprest  23620  kqdisj  23635  regr1lem  23642  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  nrmhmph  23697  fbasrn  23787  elfm2  23851  fmfnfmlem1  23857  fmco  23864  flffbas  23898  cnpflf2  23903  cnextcn  23970  metcnp3  24448  metustto  24461  cfilucfil  24467  uniioombllem3  25513  dyadmbllem  25527  mbfconstlem  25555  i1fima2  25607  itg2gt0  25689  ellimc3  25807  limcflf  25809  limcresi  25813  limciun  25822  lhop  25948  ig1peu  26108  ig1pdvds  26113  psercnlem2  26360  dvloglem  26581  efopn  26591  noetalem1  27673  madess  27802  cofcut1  27839  negsproplem2  27940  fnpreimac  32456  fsuppinisegfi  32467  gsumpart  32769  txomap  33435  zarcmplem  33482  tpr2rico  33513  pthhashvtx  34737  cvmsss2  34884  cvmopnlem  34888  cvmliftmolem1  34891  cvmliftlem15  34908  cvmlift2lem9  34921  imadifss  37068  poimirlem1  37094  poimirlem2  37095  poimirlem3  37096  poimirlem15  37108  poimirlem30  37123  dvtan  37143  heibor1lem  37282  aks6d1c2  41601  aks6d1c6lem3  41644  aks6d1c6lem5  41649  isnumbasabl  42530  isnumbasgrp  42531  dfacbasgrp  42532  trclimalb2  43156  frege81d  43177  imass2d  44638  limccog  45008  liminfgord  45142

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »