Theorem fnresdm 6604

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 6587	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6588	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3973	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 5974	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 590	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883  dom cdm 5618   ↾ cres 5620  Rel wrel 5623   Fn wfn 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-dm 5628  df-res 5630  df-fun 6487  df-fn 6488

This theorem is referenced by:  fnima  6615  fresin  6696  resasplit  6697  fresaunres2  6699  fvreseq1  6980  fnsnr  7107  fninfp  7118  fnsnsplit  7128  fsnunfv  7131  fsnunres  7132  fnsuppeq0  8132  mapunen  9074  dif1enlem  9084  fnfi  9102  canthp1lem2  10567  fseq1p1m1  13543  facnn  14228  fac0  14229  hashgval  14286  hashinf  14288  rlimres  15511  lo1res  15512  rlimresb  15518  isercolllem2  15619  isercoll  15621  ruclem4  16192  fsets  17130  sscres  17781  sscid  17782  gsumzres  19875  gsumle  20111  pwssplit1  21049  zzngim  21527  ptuncnv  23790  ptcmpfi  23796  tsmsres  24127  imasdsf1olem  24356  tmslem  24465  tmsxms  24469  imasf1oxms  24472  prdsxms  24513  tmsxps  24519  tmsxpsmopn  24520  isngp2  24580  tngngp2  24635  cnfldms  24758  cncms  25340  cnfldcusp  25342  mbfres2  25630  dvres  25896  dvres3a  25899  cpnres  25922  dvmptres3  25941  dvlip2  25980  dvgt0lem2  25988  dvne0  25996  rlimcnp2  26948  jensen  26970  eupthvdres  30323  sspg  30817  ssps  30819  sspn  30825  hhsssh  31358  fnresin  32716  padct  32810  ffsrn  32820  resf1o  32822  indf1ofs  32945  symgcom  33164  cycpmconjvlem  33222  cycpmconjslem1  33235  nsgqusf1o  33499  ply1degltdimlem  33806  cnrrext  34194  eulerpartlemt  34555  subfacp1lem3  35410  subfacp1lem5  35412  cvmliftlem11  35523  poimirlem9  37996  dvun  42836  mapfzcons1  43166  eq0rabdioph  43225  eldioph4b  43256  diophren  43258  pwssplit4  43534  tfsconcatrev  43793  dvresntr  46361  sge0split  46852  imaidfu2  49601