Theorem fssres 6734

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 6529	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6648	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5990	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5920	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3947	. . . . . 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 6529	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 237	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3907  ran crn 5652   ↾ cres 5653   Fn wfn 6520  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  fssresd  6735  fssres2  6736  fresin  6737  fresaun  6739  f1ssres  6773  resf1extb  7919  resf1ext2b  7920  f2ndf  8103  elmapssres  8852  pmresg  8856  ralxpmap  8882  mapunen  9122  fofinf1o  9277  fseqenlem1  9996  inar1  10748  gruima  10775  addnqf  10921  mulnqf  10922  fseq1p1m1  13614  injresinj  13808  seqf1olem2  14066  wrdred1  14585  rlimres  15597  lo1res  15598  vdwnnlem1  17043  fsets  17217  resmgmhm  18757  resmhm  18867  resghm  19290  gsumzres  19967  gsumzadd  19980  gsum2dlem2  20029  dpjidcl  20118  ablfac1eu  20133  abvres  20900  znf1o  21658  islindf4  21945  kgencn  23670  ptrescn  23753  hmeores  23885  tsmsres  24258  tsmsmhm  24260  tsmsadd  24261  xrge0gsumle  24948  xrge0tsms  24949  ovolicc2lem4  25636  limcdif  25992  limcflf  25997  limcmo  25998  dvres  26027  dvres3a  26030  aannenlem1  26446  logcn  26766  dvlog  26770  dvlog2  26772  logtayl  26779  dvatan  27054  atancn  27055  efrlim  27088  amgm  27109  dchrelbas2  27355  redwlklem  29924  pthdivtx  29981  hhssabloilem  31518  hhssnv  31521  wrdres  33163  gsumpart  33291  xrge0tsmsd  33301  cntmeas  34528  eulerpartlemt  34673  eulerpartlemmf  34677  eulerpartlemgvv  34678  subiwrd  34687  sseqp1  34697  poimirlem4  38130  mbfresfi  38172  mbfposadd  38173  itg2gt0cn  38181  sdclem2  38248  mzpcompact2lem  43339  eldiophb  43345  eldioph2  43350  cncfiooicclem1  46466  fouriersw  46804  sge0tsms  46953  psmeasure  47044  lindslinindimp2lem2  49091