Theorem fnresdm 6551

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3887  dom cdm 5589   ↾ cres 5591  Rel wrel 5594   Fn wfn 6428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-dm 5599  df-res 5601  df-fun 6435  df-fn 6436

This theorem is referenced by:  fnima  6563  fresin  6643  resasplit  6644  fresaunres2  6646  fvreseq1  6916  fnsnr  7037  fninfp  7046  fnsnsplit  7056  fsnunfv  7059  fsnunres  7060  fnsuppeq0  8008  mapunen  8933  dif1enlem  8943  fnfi  8964  canthp1lem2  10409  fseq1p1m1  13330  facnn  13989  fac0  13990  hashgval  14047  hashinf  14049  rlimres  15267  lo1res  15268  rlimresb  15274  isercolllem2  15377  isercoll  15379  ruclem4  15943  fsets  16870  sscres  17535  sscid  17536  gsumzres  19510  rnrhmsubrg  20056  pwssplit1  20321  zzngim  20760  ptuncnv  22958  ptcmpfi  22964  tsmsres  23295  imasdsf1olem  23526  tmslem  23637  tmslemOLD  23638  tmsxms  23642  imasf1oxms  23645  prdsxms  23686  tmsxps  23692  tmsxpsmopn  23693  isngp2  23753  tngngp2  23816  cnfldms  23939  cncms  24519  cnfldcusp  24521  mbfres2  24809  dvres  25075  dvres3a  25078  cpnres  25101  dvmptres3  25120  dvlip2  25159  dvgt0lem2  25167  dvne0  25175  rlimcnp2  26116  jensen  26138  eupthvdres  28599  sspg  29090  ssps  29092  sspn  29098  hhsssh  29631  fnresin  30961  padct  31054  ffsrn  31064  resf1o  31065  gsumle  31350  symgcom  31352  cycpmconjvlem  31408  cycpmconjslem1  31421  nsgqusf1o  31601  cnrrext  31960  indf1ofs  31994  eulerpartlemt  32338  subfacp1lem3  33144  subfacp1lem5  33146  cvmliftlem11  33257  poimirlem9  35786  mapfzcons1  40539  eq0rabdioph  40598  eldioph4b  40633  diophren  40635  pwssplit4  40914  dvresntr  43459  sge0split  43947