Theorem fnresdm 6666

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3947  dom cdm 5675   ↾ cres 5677  Rel wrel 5680   Fn wfn 6535

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-dm 5685  df-res 5687  df-fun 6542  df-fn 6543

This theorem is referenced by:  fnima  6677  fresin  6757  resasplit  6758  fresaunres2  6760  fvreseq1  7037  fnsnr  7159  fninfp  7168  fnsnsplit  7178  fsnunfv  7181  fsnunres  7182  fnsuppeq0  8173  mapunen  9142  dif1enlem  9152  dif1enlemOLD  9153  fnfi  9177  canthp1lem2  10644  fseq1p1m1  13571  facnn  14231  fac0  14232  hashgval  14289  hashinf  14291  rlimres  15498  lo1res  15499  rlimresb  15505  isercolllem2  15608  isercoll  15610  ruclem4  16173  fsets  17098  sscres  17766  sscid  17767  gsumzres  19771  rnrhmsubrg  20389  pwssplit1  20662  zzngim  21099  ptuncnv  23302  ptcmpfi  23308  tsmsres  23639  imasdsf1olem  23870  tmslem  23981  tmslemOLD  23982  tmsxms  23986  imasf1oxms  23989  prdsxms  24030  tmsxps  24036  tmsxpsmopn  24037  isngp2  24097  tngngp2  24160  cnfldms  24283  cncms  24863  cnfldcusp  24865  mbfres2  25153  dvres  25419  dvres3a  25422  cpnres  25445  dvmptres3  25464  dvlip2  25503  dvgt0lem2  25511  dvne0  25519  rlimcnp2  26460  jensen  26482  eupthvdres  29477  sspg  29968  ssps  29970  sspn  29976  hhsssh  30509  fnresin  31837  padct  31931  ffsrn  31941  resf1o  31942  gsumle  32229  symgcom  32231  cycpmconjvlem  32287  cycpmconjslem1  32300  nsgqusf1o  32515  ply1degltdimlem  32695  cnrrext  32978  indf1ofs  33012  eulerpartlemt  33358  subfacp1lem3  34161  subfacp1lem5  34163  cvmliftlem11  34274  poimirlem9  36485  mapfzcons1  41440  eq0rabdioph  41499  eldioph4b  41534  diophren  41536  pwssplit4  41816  tfsconcatrev  42083  dvresntr  44620  sge0split  45111