Theorem fnresdm 6699

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 6681	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6682	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 4067	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 6051	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 583	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976  dom cdm 5700   ↾ cres 5702  Rel wrel 5705   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-dm 5710  df-res 5712  df-fun 6575  df-fn 6576

This theorem is referenced by:  fnima  6710  fresin  6790  resasplit  6791  fresaunres2  6793  fvreseq1  7072  fnsnr  7199  fninfp  7208  fnsnsplit  7218  fsnunfv  7221  fsnunres  7222  fnsuppeq0  8233  mapunen  9212  dif1enlem  9222  dif1enlemOLD  9223  fnfi  9244  canthp1lem2  10722  fseq1p1m1  13658  facnn  14324  fac0  14325  hashgval  14382  hashinf  14384  rlimres  15604  lo1res  15605  rlimresb  15611  isercolllem2  15714  isercoll  15716  ruclem4  16282  fsets  17216  sscres  17884  sscid  17885  gsumzres  19951  pwssplit1  21081  zzngim  21594  ptuncnv  23836  ptcmpfi  23842  tsmsres  24173  imasdsf1olem  24404  tmslem  24515  tmslemOLD  24516  tmsxms  24520  imasf1oxms  24523  prdsxms  24564  tmsxps  24570  tmsxpsmopn  24571  isngp2  24631  tngngp2  24694  cnfldms  24817  cncms  25408  cnfldcusp  25410  mbfres2  25699  dvres  25966  dvres3a  25969  cpnres  25993  dvmptres3  26014  dvlip2  26054  dvgt0lem2  26062  dvne0  26070  rlimcnp2  27027  jensen  27050  eupthvdres  30267  sspg  30760  ssps  30762  sspn  30768  hhsssh  31301  fnresin  32645  padct  32733  ffsrn  32743  resf1o  32744  gsumle  33074  symgcom  33076  cycpmconjvlem  33134  cycpmconjslem1  33147  nsgqusf1o  33409  ply1degltdimlem  33635  cnrrext  33956  indf1ofs  33990  eulerpartlemt  34336  subfacp1lem3  35150  subfacp1lem5  35152  cvmliftlem11  35263  poimirlem9  37589  mapfzcons1  42673  eq0rabdioph  42732  eldioph4b  42767  diophren  42769  pwssplit4  43046  tfsconcatrev  43310  dvresntr  45839  sge0split  46330