Theorem fnresdm 6611

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901  dom cdm 5624   ↾ cres 5626  Rel wrel 5629   Fn wfn 6487

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-dm 5634  df-res 5636  df-fun 6494  df-fn 6495

This theorem is referenced by:  fnima  6622  fresin  6703  resasplit  6704  fresaunres2  6706  fvreseq1  6984  fnsnr  7109  fninfp  7120  fnsnsplit  7130  fsnunfv  7133  fsnunres  7134  fnsuppeq0  8134  mapunen  9074  dif1enlem  9084  fnfi  9102  canthp1lem2  10564  fseq1p1m1  13514  facnn  14198  fac0  14199  hashgval  14256  hashinf  14258  rlimres  15481  lo1res  15482  rlimresb  15488  isercolllem2  15589  isercoll  15591  ruclem4  16159  fsets  17096  sscres  17747  sscid  17748  gsumzres  19838  gsumle  20074  pwssplit1  21011  zzngim  21507  ptuncnv  23751  ptcmpfi  23757  tsmsres  24088  imasdsf1olem  24317  tmslem  24426  tmsxms  24430  imasf1oxms  24433  prdsxms  24474  tmsxps  24480  tmsxpsmopn  24481  isngp2  24541  tngngp2  24596  cnfldms  24719  cncms  25311  cnfldcusp  25313  mbfres2  25602  dvres  25868  dvres3a  25871  cpnres  25895  dvmptres3  25916  dvlip2  25956  dvgt0lem2  25964  dvne0  25972  rlimcnp2  26932  jensen  26955  eupthvdres  30310  sspg  30803  ssps  30805  sspn  30811  hhsssh  31344  fnresin  32702  padct  32797  ffsrn  32807  resf1o  32809  indf1ofs  32948  symgcom  33165  cycpmconjvlem  33223  cycpmconjslem1  33236  nsgqusf1o  33497  ply1degltdimlem  33779  cnrrext  34167  eulerpartlemt  34528  subfacp1lem3  35376  subfacp1lem5  35378  cvmliftlem11  35489  poimirlem9  37830  dvun  42614  mapfzcons1  42959  eq0rabdioph  43018  eldioph4b  43053  diophren  43055  pwssplit4  43331  tfsconcatrev  43590  dvresntr  46162  sge0split  46653  imaidfu2  49356