Theorem fssres 6729

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 6518	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2		fnssres 6644	. . . . 5 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶) Fn 𝐶)
3		resss 5975	. . . . . . 7 ⊢ (𝐹 ↾ 𝐶) ⊆ 𝐹
4	3	rnssi 5907	. . . . . 6 ⊢ ran (𝐹 ↾ 𝐶) ⊆ ran 𝐹
5		sstr 3958	. . . . . 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 6518	. 2 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶𝐵 ↔ ((𝐹 ↾ 𝐶) Fn 𝐶 ∧ ran (𝐹 ↾ 𝐶) ⊆ 𝐵))
11	9, 10	sylibr 234	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3917  ran crn 5642   ↾ cres 5643   Fn wfn 6509  ⟶wf 6510

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  fssresd  6730  fssres2  6731  fresin  6732  fresaun  6734  f1ssres  6766  resf1extb  7913  resf1ext2b  7914  f2ndf  8102  elmapssres  8843  pmresg  8846  ralxpmap  8872  mapunen  9116  fofinf1o  9290  fseqenlem1  9984  inar1  10735  gruima  10762  addnqf  10908  mulnqf  10909  fseq1p1m1  13566  injresinj  13756  seqf1olem2  14014  wrdred1  14532  rlimres  15531  lo1res  15532  vdwnnlem1  16973  fsets  17146  resmgmhm  18645  resmhm  18754  resghm  19171  gsumzres  19846  gsumzadd  19859  gsum2dlem2  19908  dpjidcl  19997  ablfac1eu  20012  abvres  20747  znf1o  21468  islindf4  21754  kgencn  23450  ptrescn  23533  hmeores  23665  tsmsres  24038  tsmsmhm  24040  tsmsadd  24041  xrge0gsumle  24729  xrge0tsms  24730  ovolicc2lem4  25428  limcdif  25784  limcflf  25789  limcmo  25790  dvres  25819  dvres3a  25822  aannenlem1  26243  logcn  26563  dvlog  26567  dvlog2  26569  logtayl  26576  dvatan  26852  atancn  26853  efrlim  26886  efrlimOLD  26887  amgm  26908  dchrelbas2  27155  redwlklem  29606  pthdivtx  29664  hhssabloilem  31197  hhssnv  31200  wrdres  32863  gsumpart  33004  xrge0tsmsd  33009  cntmeas  34223  eulerpartlemt  34369  eulerpartlemmf  34373  eulerpartlemgvv  34374  subiwrd  34383  sseqp1  34393  poimirlem4  37625  mbfresfi  37667  mbfposadd  37668  itg2gt0cn  37676  sdclem2  37743  mzpcompact2lem  42746  eldiophb  42752  eldioph2  42757  cncfiooicclem1  45898  fouriersw  46236  sge0tsms  46385  psmeasure  46476  sssmf  46743  lindslinindimp2lem2  48452