Theorem fssres 6726

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 6515	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6641	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5972	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5904	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3955	. . . . . 6 ⊢ ((ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵) → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
6	4, 5	mpan 690	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → ran (𝐹 ↾ 𝐶) ⊆ 𝐵)
7	2, 6	anim12i 613	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) ∧ ran 𝐹 ⊆ 𝐵) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
8	7	an32s 652	. . 3 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
9	1, 8	sylanb 581	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
10		df-f 6515	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 234	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3914  ran crn 5639   ↾ cres 5640   Fn wfn 6506  ⟶wf 6507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  fssresd  6727  fssres2  6728  fresin  6729  fresaun  6731  f1ssres  6763  resf1extb  7910  resf1ext2b  7911  f2ndf  8099  elmapssres  8840  pmresg  8843  ralxpmap  8869  mapunen  9110  fofinf1o  9283  fseqenlem1  9977  inar1  10728  gruima  10755  addnqf  10901  mulnqf  10902  fseq1p1m1  13559  injresinj  13749  seqf1olem2  14007  wrdred1  14525  rlimres  15524  lo1res  15525  vdwnnlem1  16966  fsets  17139  resmgmhm  18638  resmhm  18747  resghm  19164  gsumzres  19839  gsumzadd  19852  gsum2dlem2  19901  dpjidcl  19990  ablfac1eu  20005  abvres  20740  znf1o  21461  islindf4  21747  kgencn  23443  ptrescn  23526  hmeores  23658  tsmsres  24031  tsmsmhm  24033  tsmsadd  24034  xrge0gsumle  24722  xrge0tsms  24723  ovolicc2lem4  25421  limcdif  25777  limcflf  25782  limcmo  25783  dvres  25812  dvres3a  25815  aannenlem1  26236  logcn  26556  dvlog  26560  dvlog2  26562  logtayl  26569  dvatan  26845  atancn  26846  efrlim  26879  efrlimOLD  26880  amgm  26901  dchrelbas2  27148  redwlklem  29599  pthdivtx  29657  hhssabloilem  31190  hhssnv  31193  wrdres  32856  gsumpart  32997  xrge0tsmsd  33002  cntmeas  34216  eulerpartlemt  34362  eulerpartlemmf  34366  eulerpartlemgvv  34367  subiwrd  34376  sseqp1  34386  poimirlem4  37618  mbfresfi  37660  mbfposadd  37661  itg2gt0cn  37669  sdclem2  37736  mzpcompact2lem  42739  eldiophb  42745  eldioph2  42750  cncfiooicclem1  45891  fouriersw  46229  sge0tsms  46378  psmeasure  46469  sssmf  46736  lindslinindimp2lem2  48448