Theorem fssres 6754

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004.)

Assertion

Ref	Expression
fssres	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Proof of Theorem fssres

Step	Hyp	Ref	Expression
1		df-f 6544	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6670	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 6004	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5937	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3989	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 688	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 613	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 650	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 581	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6544	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 233	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3947  ran crn 5676   ↾ cres 5677   Fn wfn 6535  ⟶wf 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-fun 6542  df-fn 6543  df-f 6544

This theorem is referenced by:  fssresd  6755  fssres2  6756  fresin  6757  fresaun  6759  f1ssres  6792  f2ndf  8102  elmapssres  8857  pmresg  8860  ralxpmap  8886  mapunen  9142  fofinf1o  9323  fseqenlem1  10015  inar1  10766  gruima  10793  addnqf  10939  mulnqf  10940  fseq1p1m1  13571  injresinj  13749  seqf1olem2  14004  wrdred1  14506  rlimres  15498  lo1res  15499  vdwnnlem1  16924  fsets  17098  resmhm  18697  resghm  19102  gsumzres  19771  gsumzadd  19784  gsum2dlem2  19833  dpjidcl  19922  ablfac1eu  19937  abvres  20439  znf1o  21098  islindf4  21384  kgencn  23051  ptrescn  23134  hmeores  23266  tsmsres  23639  tsmsmhm  23641  tsmsadd  23642  xrge0gsumle  24340  xrge0tsms  24341  ovolicc2lem4  25028  limcdif  25384  limcflf  25389  limcmo  25390  dvres  25419  dvres3a  25422  aannenlem1  25832  logcn  26146  dvlog  26150  dvlog2  26152  logtayl  26159  dvatan  26429  atancn  26430  efrlim  26463  amgm  26484  dchrelbas2  26729  redwlklem  28917  pthdivtx  28975  hhssabloilem  30501  hhssnv  30504  wrdres  32090  gsumpart  32194  xrge0tsmsd  32196  cntmeas  33212  eulerpartlemt  33358  eulerpartlemmf  33362  eulerpartlemgvv  33363  subiwrd  33372  sseqp1  33382  poimirlem4  36480  mbfresfi  36522  mbfposadd  36523  itg2gt0cn  36531  sdclem2  36598  mzpcompact2lem  41474  eldiophb  41480  eldioph2  41485  cncfiooicclem1  44595  fouriersw  44933  sge0tsms  45082  psmeasure  45173  sssmf  45440  resmgmhm  46554  lindslinindimp2lem2  47093