Theorem fssres 6745

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3902  ran crn 5660   ↾ cres 5661   Fn wfn 6532  ⟶wf 6533

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 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  fssresd  6746  fssres2  6747  fresin  6748  fresaun  6750  f1ssres  6784  resf1extb  7935  resf1ext2b  7936  f2ndf  8121  elmapssres  8877  pmresg  8881  ralxpmap  8907  mapunen  9148  fofinf1o  9303  fseqenlem1  10031  inar1  10788  gruima  10815  addnqf  10961  mulnqf  10962  fseq1p1m1  13657  injresinj  13851  seqf1olem2  14110  wrdred1  14629  rlimres  15649  lo1res  15650  vdwnnlem1  17093  fsets  17267  resmgmhm  18819  resmhm  18935  resghm  19365  gsumzres  20042  gsumzadd  20055  gsum2dlem2  20104  dpjidcl  20193  ablfac1eu  20208  abvres  21003  znf1o  21770  islindf4  22057  kgencn  23788  ptrescn  23871  hmeores  24003  tsmsres  24376  tsmsmhm  24378  tsmsadd  24379  xrge0gsumle  25066  xrge0tsms  25067  ovolicc2lem4  25754  limcdif  26110  limcflf  26115  limcmo  26116  dvres  26145  dvres3a  26148  aannenlem1  26571  logcn  26892  dvlog  26896  dvlog2  26898  logtayl  26905  dvatan  27180  atancn  27181  efrlim  27214  amgm  27235  dchrelbas2  27481  redwlklem  30137  pthdivtx  30199  hhssabloilem  31750  hhssnv  31753  wrdres  33389  gsumpart  33511  xrge0tsmsd  33521  cntmeas  34745  eulerpartlemt  34890  eulerpartlemmf  34894  eulerpartlemgvv  34895  subiwrd  34904  sseqp1  34914  poimirlem4  38381  mbfresfi  38423  mbfposadd  38424  itg2gt0cn  38432  sdclem2  38500  mzpcompact2lem  43604  eldiophb  43610  eldioph2  43615  cncfiooicclem1  46729  fouriersw  47067  sge0tsms  47216  psmeasure  47307  lindslinindimp2lem2  49397