Theorem fnresdm 6654

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3905  dom cdm 5661   ↾ cres 5663  Rel wrel 5666   Fn wfn 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-dm 5671  df-res 5673  df-fun 6538  df-fn 6539

This theorem is referenced by:  fnima  6665  fresin  6747  resasplit  6748  fresaunres2  6750  fvreseq1  7034  fnsnr  7161  fninfp  7172  fnsnsplit  7182  fsnunfv  7185  fsnunres  7186  fnsuppeq0  8184  mapunen  9130  dif1enlem  9140  fnfi  9158  canthp1lem2  10633  fseq1p1m1  13622  facnn  14307  fac0  14308  hashgval  14365  hashinf  14367  rlimres  15605  lo1res  15606  rlimresb  15612  isercolllem2  15713  isercoll  15715  ruclem4  16285  fsets  17224  sscres  17875  sscid  17876  gsumzres  19974  gsumle  20210  pwssplit1  21180  zzngim  21702  ptuncnv  23964  ptcmpfi  23970  tsmsres  24301  imasdsf1olem  24530  tmslem  24639  tmsxms  24643  imasf1oxms  24646  prdsxms  24687  tmsxps  24693  tmsxpsmopn  24694  isngp2  24754  tngngp2  24809  cnfldms  24932  cncms  25514  cnfldcusp  25516  mbfres2  25804  dvres  26070  dvres3a  26073  cpnres  26096  dvmptres3  26115  dvlip2  26154  dvgt0lem2  26162  dvne0  26170  rlimcnp2  27131  jensen  27153  eupthvdres  30586  sspg  31080  ssps  31082  sspn  31088  hhsssh  31621  fnresin  32969  padct  33063  ffsrn  33073  resf1o  33075  indf1ofs  33186  symgcom  33403  cycpmconjvlem  33461  cycpmconjslem1  33474  nsgqusf1o  33725  ply1degltdimlem  34012  cnrrext  34400  eulerpartlemt  34761  subfacp1lem3  35674  subfacp1lem5  35676  cvmliftlem11  35787  poimirlem9  38280  dvun  43120  mapfzcons1  43448  eq0rabdioph  43507  eldioph4b  43538  diophren  43540  pwssplit4  43816  tfsconcatrev  44075  dvresntr  46632  sge0split  47123  imaidfu2  49889