Theorem fssres 6756

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 6546	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6672	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 6005	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5938	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3989	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 686	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 611	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 648	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 579	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6546	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 233	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 394   ⊆ wss 3947  ran crn 5676   ↾ cres 5677   Fn wfn 6537  ⟶wf 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  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 6544  df-fn 6545  df-f 6546

This theorem is referenced by:  fssresd  6757  fssres2  6758  fresin  6759  fresaun  6761  f1ssres  6794  f2ndf  8108  elmapssres  8863  pmresg  8866  ralxpmap  8892  mapunen  9148  fofinf1o  9329  fseqenlem1  10021  inar1  10772  gruima  10799  addnqf  10945  mulnqf  10946  fseq1p1m1  13579  injresinj  13757  seqf1olem2  14012  wrdred1  14514  rlimres  15506  lo1res  15507  vdwnnlem1  16932  fsets  17106  resmgmhm  18636  resmhm  18737  resghm  19146  gsumzres  19818  gsumzadd  19831  gsum2dlem2  19880  dpjidcl  19969  ablfac1eu  19984  abvres  20590  znf1o  21326  islindf4  21612  kgencn  23280  ptrescn  23363  hmeores  23495  tsmsres  23868  tsmsmhm  23870  tsmsadd  23871  xrge0gsumle  24569  xrge0tsms  24570  ovolicc2lem4  25269  limcdif  25625  limcflf  25630  limcmo  25631  dvres  25660  dvres3a  25663  aannenlem1  26077  logcn  26391  dvlog  26395  dvlog2  26397  logtayl  26404  dvatan  26676  atancn  26677  efrlim  26710  amgm  26731  dchrelbas2  26976  redwlklem  29195  pthdivtx  29253  hhssabloilem  30781  hhssnv  30784  wrdres  32370  gsumpart  32477  xrge0tsmsd  32479  cntmeas  33522  eulerpartlemt  33668  eulerpartlemmf  33672  eulerpartlemgvv  33673  subiwrd  33682  sseqp1  33692  poimirlem4  36795  mbfresfi  36837  mbfposadd  36838  itg2gt0cn  36846  sdclem2  36913  mzpcompact2lem  41791  eldiophb  41797  eldioph2  41802  cncfiooicclem1  44907  fouriersw  45245  sge0tsms  45394  psmeasure  45485  sssmf  45752  lindslinindimp2lem2  47227