Theorem fnresdm 6601

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 6584	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6585	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3994	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 5973	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 584	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3903  dom cdm 5619   ↾ cres 5621  Rel wrel 5624   Fn wfn 6477

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626  df-dm 5629  df-res 5631  df-fun 6484  df-fn 6485

This theorem is referenced by:  fnima  6612  fresin  6693  resasplit  6694  fresaunres2  6696  fvreseq1  6973  fnsnr  7099  fninfp  7110  fnsnsplit  7120  fsnunfv  7123  fsnunres  7124  fnsuppeq0  8125  mapunen  9063  dif1enlem  9073  fnfi  9092  canthp1lem2  10547  fseq1p1m1  13501  facnn  14182  fac0  14183  hashgval  14240  hashinf  14242  rlimres  15465  lo1res  15466  rlimresb  15472  isercolllem2  15573  isercoll  15575  ruclem4  16143  fsets  17080  sscres  17730  sscid  17731  gsumzres  19788  gsumle  20024  pwssplit1  20963  zzngim  21459  ptuncnv  23692  ptcmpfi  23698  tsmsres  24029  imasdsf1olem  24259  tmslem  24368  tmsxms  24372  imasf1oxms  24375  prdsxms  24416  tmsxps  24422  tmsxpsmopn  24423  isngp2  24483  tngngp2  24538  cnfldms  24661  cncms  25253  cnfldcusp  25255  mbfres2  25544  dvres  25810  dvres3a  25813  cpnres  25837  dvmptres3  25858  dvlip2  25898  dvgt0lem2  25906  dvne0  25914  rlimcnp2  26874  jensen  26897  eupthvdres  30179  sspg  30672  ssps  30674  sspn  30680  hhsssh  31213  fnresin  32568  padct  32662  ffsrn  32672  resf1o  32673  indf1ofs  32809  symgcom  33025  cycpmconjvlem  33083  cycpmconjslem1  33096  nsgqusf1o  33353  ply1degltdimlem  33589  cnrrext  33977  eulerpartlemt  34339  subfacp1lem3  35155  subfacp1lem5  35157  cvmliftlem11  35268  poimirlem9  37609  dvun  42332  mapfzcons1  42690  eq0rabdioph  42749  eldioph4b  42784  diophren  42786  pwssplit4  43062  tfsconcatrev  43321  dvresntr  45899  sge0split  46390  imaidfu2  49096