Theorem fnresdm 6662

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3931  dom cdm 5659   ↾ cres 5661  Rel wrel 5664   Fn wfn 6531

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-rel 5666  df-dm 5669  df-res 5671  df-fun 6538  df-fn 6539

This theorem is referenced by:  fnima  6673  fresin  6752  resasplit  6753  fresaunres2  6755  fvreseq1  7034  fnsnr  7160  fninfp  7171  fnsnsplit  7181  fsnunfv  7184  fsnunres  7185  fnsuppeq0  8196  mapunen  9165  dif1enlem  9175  dif1enlemOLD  9176  fnfi  9197  canthp1lem2  10672  fseq1p1m1  13620  facnn  14298  fac0  14299  hashgval  14356  hashinf  14358  rlimres  15579  lo1res  15580  rlimresb  15586  isercolllem2  15687  isercoll  15689  ruclem4  16257  fsets  17193  sscres  17841  sscid  17842  gsumzres  19895  pwssplit1  21022  zzngim  21518  ptuncnv  23750  ptcmpfi  23756  tsmsres  24087  imasdsf1olem  24317  tmslem  24426  tmsxms  24430  imasf1oxms  24433  prdsxms  24474  tmsxps  24480  tmsxpsmopn  24481  isngp2  24541  tngngp2  24596  cnfldms  24719  cncms  25312  cnfldcusp  25314  mbfres2  25603  dvres  25869  dvres3a  25872  cpnres  25896  dvmptres3  25917  dvlip2  25957  dvgt0lem2  25965  dvne0  25973  rlimcnp2  26933  jensen  26956  eupthvdres  30221  sspg  30714  ssps  30716  sspn  30722  hhsssh  31255  fnresin  32609  padct  32702  ffsrn  32711  resf1o  32712  indf1ofs  32848  gsumle  33097  symgcom  33099  cycpmconjvlem  33157  cycpmconjslem1  33170  nsgqusf1o  33436  ply1degltdimlem  33667  cnrrext  34046  eulerpartlemt  34408  subfacp1lem3  35209  subfacp1lem5  35211  cvmliftlem11  35322  poimirlem9  37658  dvun  42369  mapfzcons1  42707  eq0rabdioph  42766  eldioph4b  42801  diophren  42803  pwssplit4  43080  tfsconcatrev  43339  dvresntr  45914  sge0split  46405  imaidfu2  49037