Theorem fnresdm 6617

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 6600	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6601	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3980	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 5987	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 585	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889  dom cdm 5631   ↾ cres 5633  Rel wrel 5636   Fn wfn 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638  df-dm 5641  df-res 5643  df-fun 6500  df-fn 6501

This theorem is referenced by:  fnima  6628  fresin  6709  resasplit  6710  fresaunres2  6712  fvreseq1  6991  fnsnr  7118  fninfp  7129  fnsnsplit  7139  fsnunfv  7142  fsnunres  7143  fnsuppeq0  8142  mapunen  9084  dif1enlem  9094  fnfi  9112  canthp1lem2  10576  fseq1p1m1  13552  facnn  14237  fac0  14238  hashgval  14295  hashinf  14297  rlimres  15520  lo1res  15521  rlimresb  15527  isercolllem2  15628  isercoll  15630  ruclem4  16201  fsets  17139  sscres  17790  sscid  17791  gsumzres  19884  gsumle  20120  pwssplit1  21054  zzngim  21532  ptuncnv  23772  ptcmpfi  23778  tsmsres  24109  imasdsf1olem  24338  tmslem  24447  tmsxms  24451  imasf1oxms  24454  prdsxms  24495  tmsxps  24501  tmsxpsmopn  24502  isngp2  24562  tngngp2  24617  cnfldms  24740  cncms  25322  cnfldcusp  25324  mbfres2  25612  dvres  25878  dvres3a  25881  cpnres  25904  dvmptres3  25923  dvlip2  25962  dvgt0lem2  25970  dvne0  25978  rlimcnp2  26930  jensen  26952  eupthvdres  30305  sspg  30799  ssps  30801  sspn  30807  hhsssh  31340  fnresin  32697  padct  32791  ffsrn  32801  resf1o  32803  indf1ofs  32926  symgcom  33144  cycpmconjvlem  33202  cycpmconjslem1  33215  nsgqusf1o  33476  ply1degltdimlem  33766  cnrrext  34154  eulerpartlemt  34515  subfacp1lem3  35364  subfacp1lem5  35366  cvmliftlem11  35477  poimirlem9  37950  dvun  42791  mapfzcons1  43149  eq0rabdioph  43208  eldioph4b  43239  diophren  43241  pwssplit4  43517  tfsconcatrev  43776  dvresntr  46346  sge0split  46837  imaidfu2  49586