Theorem fnresdm 6640

Description: A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)

Assertion

Ref	Expression
fnresdm	⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Proof of Theorem fnresdm

Step	Hyp	Ref	Expression
1		fnrel 6623	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6624	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3994	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 6008	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 593	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1560   ⊆ wss 3904  dom cdm 5647   ↾ cres 5649  Rel wrel 5652   Fn wfn 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-rel 5654  df-dm 5657  df-res 5659  df-fun 6523  df-fn 6524

This theorem is referenced by:  fnima  6651  fresin  6733  resasplit  6734  fresaunres2  6736  fvreseq1  7020  fnsnr  7147  fninfp  7158  fnsnsplit  7168  fsnunfv  7171  fsnunres  7172  fnsuppeq0  8172  mapunen  9118  dif1enlem  9128  fnfi  9146  canthp1lem2  10611  fseq1p1m1  13603  facnn  14288  fac0  14289  hashgval  14346  hashinf  14348  rlimres  15585  lo1res  15586  rlimresb  15592  isercolllem2  15693  isercoll  15695  ruclem4  16266  fsets  17205  sscres  17856  sscid  17857  gsumzres  19949  gsumle  20185  pwssplit1  21123  zzngim  21601  ptuncnv  23864  ptcmpfi  23870  tsmsres  24201  imasdsf1olem  24430  tmslem  24539  tmsxms  24543  imasf1oxms  24546  prdsxms  24587  tmsxps  24593  tmsxpsmopn  24594  isngp2  24654  tngngp2  24709  cnfldms  24832  cncms  25414  cnfldcusp  25416  mbfres2  25704  dvres  25970  dvres3a  25973  cpnres  25996  dvmptres3  26015  dvlip2  26054  dvgt0lem2  26062  dvne0  26070  rlimcnp2  27028  jensen  27050  eupthvdres  30434  sspg  30928  ssps  30930  sspn  30936  hhsssh  31469  fnresin  32823  padct  32917  ffsrn  32927  resf1o  32929  indf1ofs  33041  symgcom  33260  cycpmconjvlem  33318  cycpmconjslem1  33331  nsgqusf1o  33599  ply1degltdimlem  33916  cnrrext  34304  eulerpartlemt  34665  subfacp1lem3  35529  subfacp1lem5  35531  cvmliftlem11  35642  poimirlem9  38125  dvun  42965  mapfzcons1  43295  eq0rabdioph  43354  eldioph4b  43385  diophren  43387  pwssplit4  43663  tfsconcatrev  43922  dvresntr  46489  sge0split  46980  imaidfu2  49729