Theorem fnresdm 6600

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3897  dom cdm 5614   ↾ cres 5616  Rel wrel 5619   Fn wfn 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-xp 5620  df-rel 5621  df-dm 5624  df-res 5626  df-fun 6483  df-fn 6484

This theorem is referenced by:  fnima  6611  fresin  6692  resasplit  6693  fresaunres2  6695  fvreseq1  6972  fnsnr  7097  fninfp  7108  fnsnsplit  7118  fsnunfv  7121  fsnunres  7122  fnsuppeq0  8122  mapunen  9059  dif1enlem  9069  fnfi  9087  canthp1lem2  10544  fseq1p1m1  13498  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  19821  gsumle  20057  pwssplit1  20993  zzngim  21489  ptuncnv  23722  ptcmpfi  23728  tsmsres  24059  imasdsf1olem  24288  tmslem  24397  tmsxms  24401  imasf1oxms  24404  prdsxms  24445  tmsxps  24451  tmsxpsmopn  24452  isngp2  24512  tngngp2  24567  cnfldms  24690  cncms  25282  cnfldcusp  25284  mbfres2  25573  dvres  25839  dvres3a  25842  cpnres  25866  dvmptres3  25887  dvlip2  25927  dvgt0lem2  25935  dvne0  25943  rlimcnp2  26903  jensen  26926  eupthvdres  30215  sspg  30708  ssps  30710  sspn  30716  hhsssh  31249  fnresin  32607  padct  32701  ffsrn  32711  resf1o  32713  indf1ofs  32847  symgcom  33052  cycpmconjvlem  33110  cycpmconjslem1  33123  nsgqusf1o  33381  ply1degltdimlem  33635  cnrrext  34023  eulerpartlemt  34384  subfacp1lem3  35226  subfacp1lem5  35228  cvmliftlem11  35339  poimirlem9  37677  dvun  42400  mapfzcons1  42758  eq0rabdioph  42817  eldioph4b  42852  diophren  42854  pwssplit4  43130  tfsconcatrev  43389  dvresntr  45964  sge0split  46455  imaidfu2  49151