Theorem fssres 6740

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

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

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 3902  df-un 3904  df-in 3906  df-ss 3916  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 6533  df-fn 6534  df-f 6535

This theorem is used by:  fssresd  6741  fssres2  6742  fresin  6743  fresaun  6745  f1ssres  6779  resf1extb  7935  resf1ext2b  7936  f2ndf  8120  tz7.48lem  8434  elmapssres  8878  pmresg  8882  ralxpmap  8908  mapunen  9149  fofinf1o  9305  fseqenlem1  10084  inar1  10841  gruima  10868  addnqf  11014  mulnqf  11015  fseq1p1m1  13712  injresinj  13906  seqf1olem2  14165  wrdred1  14685  rlimres  15705  lo1res  15706  vdwnnlem1  17153  fsets  17327  resmgmhm  18880  resmhm  18996  resghm  19426  gsumzres  20103  gsumzadd  20116  gsum2dlem2  20165  dpjidcl  20254  ablfac1eu  20269  abvres  21068  znf1o  21837  islindf4  22124  kgencn  23855  ptrescn  23938  hmeores  24070  tsmsres  24443  tsmsmhm  24445  tsmsadd  24446  xrge0gsumle  25133  xrge0tsms  25134  ovolicc2lem4  25821  limcdif  26176  limcflf  26181  limcmo  26182  dvres  26211  dvres3a  26214  aannenlem1  26637  logcn  26957  dvlog  26961  dvlog2  26963  logtayl  26970  dvatan  27245  atancn  27246  efrlim  27279  amgm  27300  dchrelbas2  27546  redwlklem  30232  pthdivtx  30294  hhssabloilem  31845  hhssnv  31848  wrdres  33484  gsumpart  33606  xrge0tsmsd  33616  cntmeas  34841  eulerpartlemt  34986  eulerpartlemmf  34990  eulerpartlemgvv  34991  subiwrd  35000  sseqp1  35010  poimirlem4  38510  mbfresfi  38552  mbfposadd  38553  itg2gt0cn  38561  sdclem2  38644  mzpcompact2lem  43715  eldiophb  43721  eldioph2  43726  cncfiooicclem1  46847  fouriersw  47185  sge0tsms  47334  psmeasure  47425  lindslinindimp2lem2  49515