Theorem fssres 6746

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 6542	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6660	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 6002	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5932	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3946	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 702	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 624	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 664	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 592	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6542	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 237	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3906  ran crn 5664   ↾ cres 5665   Fn wfn 6533  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  fssresd  6747  fssres2  6748  fresin  6749  fresaun  6751  f1ssres  6785  resf1extb  7932  resf1ext2b  7933  f2ndf  8116  elmapssres  8865  pmresg  8869  ralxpmap  8895  mapunen  9135  fofinf1o  9290  fseqenlem1  10009  inar1  10761  gruima  10788  addnqf  10934  mulnqf  10935  fseq1p1m1  13628  injresinj  13822  seqf1olem2  14080  wrdred1  14599  rlimres  15611  lo1res  15612  vdwnnlem1  17056  fsets  17230  resmgmhm  18770  resmhm  18880  resghm  19303  gsumzres  19980  gsumzadd  19993  gsum2dlem2  20042  dpjidcl  20131  ablfac1eu  20146  abvres  20915  znf1o  21682  islindf4  21969  kgencn  23694  ptrescn  23777  hmeores  23909  tsmsres  24282  tsmsmhm  24284  tsmsadd  24285  xrge0gsumle  24972  xrge0tsms  24973  ovolicc2lem4  25660  limcdif  26016  limcflf  26021  limcmo  26022  dvres  26051  dvres3a  26054  aannenlem1  26472  logcn  26793  dvlog  26797  dvlog2  26799  logtayl  26806  dvatan  27081  atancn  27082  efrlim  27115  amgm  27136  dchrelbas2  27382  redwlklem  30000  pthdivtx  30057  hhssabloilem  31594  hhssnv  31597  wrdres  33236  gsumpart  33364  xrge0tsmsd  33374  cntmeas  34597  eulerpartlemt  34742  eulerpartlemmf  34746  eulerpartlemgvv  34747  subiwrd  34756  sseqp1  34766  poimirlem4  38256  mbfresfi  38298  mbfposadd  38299  itg2gt0cn  38307  sdclem2  38374  mzpcompact2lem  43465  eldiophb  43471  eldioph2  43476  cncfiooicclem1  46590  fouriersw  46928  sge0tsms  47077  psmeasure  47168  lindslinindimp2lem2  49222