Theorem fssres 6749

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 6543	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6663	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5992	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5922	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3937	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 703	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 625	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 665	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 593	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6543	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 237	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3914  ran crn 5652   ↾ cres 5653   Fn wfn 6534  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3900  df-un 3902  df-in 3904  df-ss 3915  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-fun 6541  df-fn 6542  df-f 6543

This theorem is used by:  fssresd  6750  fssres2  6751  fresin  6752  fresaun  6754  f1ssres  6788  resf1extb  7947  resf1ext2b  7948  f2ndf  8132  tz7.48lem  8451  elmapssres  8895  pmresg  8899  ralxpmap  8925  mapunen  9166  fofinf1o  9322  fseqenlem1  10104  inar1  10861  gruima  10888  addnqf  11034  mulnqf  11035  fseq1p1m1  13733  injresinj  13927  seqf1olem2  14186  wrdred1  14706  rlimres  15726  lo1res  15727  vdwnnlem1  17174  fsets  17348  resmgmhm  18901  resmhm  19017  resghm  19447  gsumzres  20124  gsumzadd  20137  gsum2dlem2  20186  dpjidcl  20275  ablfac1eu  20290  abvres  21089  znf1o  21858  islindf4  22145  kgencn  23876  ptrescn  23959  hmeores  24091  tsmsres  24464  tsmsmhm  24466  tsmsadd  24467  xrge0gsumle  25154  xrge0tsms  25155  ovolicc2lem4  25842  limcdif  26197  limcflf  26202  limcmo  26203  dvres  26232  dvres3a  26235  aannenlem1  26656  logcn  26976  dvlog  26980  dvlog2  26982  logtayl  26989  dvatan  27264  atancn  27265  efrlim  27298  amgm  27319  dchrelbas2  27565  redwlklem  30251  pthdivtx  30313  hhssabloilem  31864  hhssnv  31867  wrdres  33503  gsumpart  33625  xrge0tsmsd  33635  cntmeas  34860  eulerpartlemt  35004  eulerpartlemmf  35008  eulerpartlemgvv  35009  subiwrd  35018  sseqp1  35028  werankwe  35740  acwer1prc  35761  poimirlem4  38544  mbfresfi  38586  mbfposadd  38587  itg2gt0cn  38595  sdclem2  38678  mzpcompact2lem  43763  eldiophb  43769  eldioph2  43774  cncfiooicclem1  46904  fouriersw  47242  sge0tsms  47391  psmeasure  47482  lindslinindimp2lem2  49572