Theorem fssres 6751

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3908  ran crn 5667   ↾ cres 5668   Fn wfn 6538  ⟶wf 6539

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  fssresd  6752  fssres2  6753  fresin  6754  fresaun  6756  f1ssres  6790  resf1extb  7940  resf1ext2b  7941  f2ndf  8124  elmapssres  8873  pmresg  8877  ralxpmap  8903  mapunen  9144  fofinf1o  9299  fseqenlem1  10027  inar1  10778  gruima  10805  addnqf  10951  mulnqf  10952  fseq1p1m1  13645  injresinj  13839  seqf1olem2  14098  wrdred1  14617  rlimres  15635  lo1res  15636  vdwnnlem1  17080  fsets  17254  resmgmhm  18798  resmhm  18910  resghm  19333  gsumzres  20010  gsumzadd  20023  gsum2dlem2  20072  dpjidcl  20161  ablfac1eu  20176  abvres  20971  znf1o  21738  islindf4  22025  kgencn  23750  ptrescn  23833  hmeores  23965  tsmsres  24338  tsmsmhm  24340  tsmsadd  24341  xrge0gsumle  25028  xrge0tsms  25029  ovolicc2lem4  25716  limcdif  26072  limcflf  26077  limcmo  26078  dvres  26107  dvres3a  26110  aannenlem1  26528  logcn  26849  dvlog  26853  dvlog2  26855  logtayl  26862  dvatan  27137  atancn  27138  efrlim  27171  amgm  27192  dchrelbas2  27438  redwlklem  30056  pthdivtx  30113  hhssabloilem  31650  hhssnv  31653  wrdres  33292  gsumpart  33414  xrge0tsmsd  33424  cntmeas  34648  eulerpartlemt  34793  eulerpartlemmf  34797  eulerpartlemgvv  34798  subiwrd  34807  sseqp1  34817  poimirlem4  38316  mbfresfi  38358  mbfposadd  38359  itg2gt0cn  38367  sdclem2  38434  mzpcompact2lem  43523  eldiophb  43529  eldioph2  43534  cncfiooicclem1  46648  fouriersw  46986  sge0tsms  47135  psmeasure  47226  lindslinindimp2lem2  49280