Theorem fssres 6700

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 6496	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6615	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5960	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5889	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3930	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 696	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 619	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 658	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 587	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6496	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 235	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3890  ran crn 5626   ↾ cres 5627   Fn wfn 6487  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fssresd  6701  fssres2  6702  fresin  6703  fresaun  6705  f1ssres  6737  resf1extb  7881  resf1ext2b  7882  f2ndf  8066  elmapssres  8811  pmresg  8815  ralxpmap  8841  mapunen  9081  fofinf1o  9239  fseqenlem1  9944  inar1  10696  gruima  10723  addnqf  10869  mulnqf  10870  fseq1p1m1  13550  injresinj  13744  seqf1olem2  14002  wrdred1  14520  rlimres  15518  lo1res  15519  vdwnnlem1  16964  fsets  17137  resmgmhm  18677  resmhm  18786  resghm  19205  gsumzres  19882  gsumzadd  19895  gsum2dlem2  19944  dpjidcl  20033  ablfac1eu  20048  abvres  20810  znf1o  21533  islindf4  21820  kgencn  23546  ptrescn  23629  hmeores  23761  tsmsres  24134  tsmsmhm  24136  tsmsadd  24137  xrge0gsumle  24824  xrge0tsms  24825  ovolicc2lem4  25512  limcdif  25868  limcflf  25873  limcmo  25874  dvres  25903  dvres3a  25906  aannenlem1  26319  logcn  26636  dvlog  26640  dvlog2  26642  logtayl  26649  dvatan  26924  atancn  26925  efrlim  26958  amgm  26979  dchrelbas2  27225  redwlklem  29763  pthdivtx  29820  hhssabloilem  31357  hhssnv  31360  wrdres  33021  gsumpart  33151  xrge0tsmsd  33161  cntmeas  34417  eulerpartlemt  34562  eulerpartlemmf  34566  eulerpartlemgvv  34567  subiwrd  34576  sseqp1  34586  poimirlem4  37998  mbfresfi  38040  mbfposadd  38041  itg2gt0cn  38049  sdclem2  38116  mzpcompact2lem  43207  eldiophb  43213  eldioph2  43218  cncfiooicclem1  46343  fouriersw  46681  sge0tsms  46830  psmeasure  46921  sssmf  47188  lindslinindimp2lem2  48957