Theorem fssres 6624

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 6422	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6539	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5905	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5838	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3925	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 686	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 612	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 648	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 580	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6422	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 233	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3883  ran crn 5581   ↾ cres 5582   Fn wfn 6413  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  fssresd  6625  fssres2  6626  fresin  6627  fresaun  6629  f1ssres  6662  f2ndf  7932  elmapssres  8613  pmresg  8616  ralxpmap  8642  mapunen  8882  fofinf1o  9024  fseqenlem1  9711  inar1  10462  gruima  10489  addnqf  10635  mulnqf  10636  fseq1p1m1  13259  injresinj  13436  seqf1olem2  13691  wrdred1  14191  rlimres  15195  lo1res  15196  vdwnnlem1  16624  fsets  16798  resmhm  18374  resghm  18765  gsumzres  19425  gsumzadd  19438  gsum2dlem2  19487  dpjidcl  19576  ablfac1eu  19591  abvres  20014  znf1o  20671  islindf4  20955  kgencn  22615  ptrescn  22698  hmeores  22830  tsmsres  23203  tsmsmhm  23205  tsmsadd  23206  xrge0gsumle  23902  xrge0tsms  23903  ovolicc2lem4  24589  limcdif  24945  limcflf  24950  limcmo  24951  dvres  24980  dvres3a  24983  aannenlem1  25393  logcn  25707  dvlog  25711  dvlog2  25713  logtayl  25720  dvatan  25990  atancn  25991  efrlim  26024  amgm  26045  dchrelbas2  26290  redwlklem  27941  pthdivtx  27998  hhssabloilem  29524  hhssnv  29527  wrdres  31113  gsumpart  31217  xrge0tsmsd  31219  cntmeas  32094  eulerpartlemt  32238  eulerpartlemmf  32242  eulerpartlemgvv  32243  subiwrd  32252  sseqp1  32262  poimirlem4  35708  mbfresfi  35750  mbfposadd  35751  itg2gt0cn  35759  sdclem2  35827  mzpcompact2lem  40489  eldiophb  40495  eldioph2  40500  cncfiooicclem1  43324  fouriersw  43662  sge0tsms  43808  psmeasure  43899  sssmf  44161  resmgmhm  45240  lindslinindimp2lem2  45688