Theorem fnresdm 6655

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 6638	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6639	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 4003	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 18	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 6022	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 595	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913  dom cdm 5662   ↾ cres 5664  Rel wrel 5667   Fn wfn 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-rel 5669  df-dm 5672  df-res 5674  df-fun 6539  df-fn 6540

This theorem is referenced by:  fnima  6666  fresin  6748  resasplit  6749  fresaunres2  6751  fvreseq1  7035  fnsnr  7162  fninfp  7173  fnsnsplit  7183  fsnunfv  7186  fsnunres  7187  fnsuppeq0  8187  mapunen  9133  dif1enlem  9143  fnfi  9161  canthp1lem2  10637  fseq1p1m1  13625  facnn  14310  fac0  14311  hashgval  14368  hashinf  14370  rlimres  15608  lo1res  15609  rlimresb  15615  isercolllem2  15716  isercoll  15718  ruclem4  16289  fsets  17228  sscres  17879  sscid  17880  gsumzres  19978  gsumle  20214  pwssplit1  21157  zzngim  21670  ptuncnv  23932  ptcmpfi  23938  tsmsres  24269  imasdsf1olem  24498  tmslem  24607  tmsxms  24611  imasf1oxms  24614  prdsxms  24655  tmsxps  24661  tmsxpsmopn  24662  isngp2  24722  tngngp2  24777  cnfldms  24900  cncms  25482  cnfldcusp  25484  mbfres2  25772  dvres  26038  dvres3a  26041  cpnres  26064  dvmptres3  26083  dvlip2  26122  dvgt0lem2  26130  dvne0  26138  rlimcnp2  27096  jensen  27118  eupthvdres  30526  sspg  31020  ssps  31022  sspn  31028  hhsssh  31561  fnresin  32909  padct  33003  ffsrn  33013  resf1o  33015  indf1ofs  33126  symgcom  33343  cycpmconjvlem  33401  cycpmconjslem1  33414  nsgqusf1o  33668  ply1degltdimlem  33956  cnrrext  34344  eulerpartlemt  34705  subfacp1lem3  35572  subfacp1lem5  35574  cvmliftlem11  35685  poimirlem9  38167  dvun  43009  mapfzcons1  43339  eq0rabdioph  43398  eldioph4b  43429  diophren  43431  pwssplit4  43707  tfsconcatrev  43966  dvresntr  46523  sge0split  47014  imaidfu2  49773