Theorem fnresdm 6612

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890  dom cdm 5625   ↾ cres 5627  Rel wrel 5630   Fn wfn 6488

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5631  df-rel 5632  df-dm 5635  df-res 5637  df-fun 6495  df-fn 6496

This theorem is referenced by:  fnima  6623  fresin  6704  resasplit  6705  fresaunres2  6707  fvreseq1  6986  fnsnr  7112  fninfp  7123  fnsnsplit  7133  fsnunfv  7136  fsnunres  7137  fnsuppeq0  8136  mapunen  9078  dif1enlem  9088  fnfi  9106  canthp1lem2  10570  fseq1p1m1  13546  facnn  14231  fac0  14232  hashgval  14289  hashinf  14291  rlimres  15514  lo1res  15515  rlimresb  15521  isercolllem2  15622  isercoll  15624  ruclem4  16195  fsets  17133  sscres  17784  sscid  17785  gsumzres  19878  gsumle  20114  pwssplit1  21049  zzngim  21545  ptuncnv  23785  ptcmpfi  23791  tsmsres  24122  imasdsf1olem  24351  tmslem  24460  tmsxms  24464  imasf1oxms  24467  prdsxms  24508  tmsxps  24514  tmsxpsmopn  24515  isngp2  24575  tngngp2  24630  cnfldms  24753  cncms  25335  cnfldcusp  25337  mbfres2  25625  dvres  25891  dvres3a  25894  cpnres  25917  dvmptres3  25936  dvlip2  25975  dvgt0lem2  25983  dvne0  25991  rlimcnp2  26946  jensen  26969  eupthvdres  30323  sspg  30817  ssps  30819  sspn  30825  hhsssh  31358  fnresin  32715  padct  32809  ffsrn  32819  resf1o  32821  indf1ofs  32944  symgcom  33162  cycpmconjvlem  33220  cycpmconjslem1  33233  nsgqusf1o  33494  ply1degltdimlem  33785  cnrrext  34173  eulerpartlemt  34534  subfacp1lem3  35383  subfacp1lem5  35385  cvmliftlem11  35496  poimirlem9  37967  dvun  42808  mapfzcons1  43166  eq0rabdioph  43225  eldioph4b  43260  diophren  43262  pwssplit4  43538  tfsconcatrev  43797  dvresntr  46367  sge0split  46858  imaidfu2  49601