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 5991	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5921	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3916	. . . . . 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 3895  ran crn 5651   ↾ cres 5652   Fn wfn 6534  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  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  8134  tz7.48lem  8454  elmapssres  8898  pmresg  8902  ralxpmap  8928  mapunen  9169  fofinf1o  9325  fseqenlem1  10107  inar1  10864  gruima  10891  addnqf  11037  mulnqf  11038  fseq1p1m1  13736  injresinj  13930  seqf1olem2  14189  wrdred1  14709  rlimres  15731  lo1res  15732  vdwnnlem1  17179  fsets  17353  resmgmhm  18906  resmhm  19022  resghm  19452  gsumzres  20129  gsumzadd  20142  gsum2dlem2  20191  dpjidcl  20280  ablfac1eu  20295  abvres  21094  znf1o  21863  islindf4  22150  kgencn  23881  ptrescn  23964  hmeores  24096  tsmsres  24469  tsmsmhm  24471  tsmsadd  24472  xrge0gsumle  25159  xrge0tsms  25160  ovolicc2lem4  25847  limcdif  26202  limcflf  26207  limcmo  26208  dvres  26237  dvres3a  26240  aannenlem1  26661  logcn  26981  dvlog  26985  dvlog2  26987  logtayl  26994  dvatan  27269  atancn  27270  efrlim  27303  amgm  27324  dchrelbas2  27570  redwlklem  30256  pthdivtx  30318  hhssabloilem  31869  hhssnv  31872  wrdres  33549  gsumpart  33671  xrge0tsmsd  33681  cntmeas  34906  eulerpartlemt  35050  eulerpartlemmf  35054  eulerpartlemgvv  35055  subiwrd  35064  sseqp1  35074  werankwe  35792  werankwe2  35793  acwer1prc  35817  poimirlem4  38636  mbfresfi  38678  mbfposadd  38679  itg2gt0cn  38687  sdclem2  38770  mzpcompact2lem  43856  eldiophb  43862  eldioph2  43867  cncfiooicclem1  46997  fouriersw  47335  sge0tsms  47484  psmeasure  47575  lindslinindimp2lem2  49665