Theorem fnresdm 6687

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951  dom cdm 5685   ↾ cres 5687  Rel wrel 5690   Fn wfn 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-dm 5695  df-res 5697  df-fun 6563  df-fn 6564

This theorem is referenced by:  fnima  6698  fresin  6777  resasplit  6778  fresaunres2  6780  fvreseq1  7059  fnsnr  7185  fninfp  7194  fnsnsplit  7204  fsnunfv  7207  fsnunres  7208  fnsuppeq0  8217  mapunen  9186  dif1enlem  9196  dif1enlemOLD  9197  fnfi  9218  canthp1lem2  10693  fseq1p1m1  13638  facnn  14314  fac0  14315  hashgval  14372  hashinf  14374  rlimres  15594  lo1res  15595  rlimresb  15601  isercolllem2  15702  isercoll  15704  ruclem4  16270  fsets  17206  sscres  17867  sscid  17868  gsumzres  19927  pwssplit1  21058  zzngim  21571  ptuncnv  23815  ptcmpfi  23821  tsmsres  24152  imasdsf1olem  24383  tmslem  24494  tmslemOLD  24495  tmsxms  24499  imasf1oxms  24502  prdsxms  24543  tmsxps  24549  tmsxpsmopn  24550  isngp2  24610  tngngp2  24673  cnfldms  24796  cncms  25389  cnfldcusp  25391  mbfres2  25680  dvres  25946  dvres3a  25949  cpnres  25973  dvmptres3  25994  dvlip2  26034  dvgt0lem2  26042  dvne0  26050  rlimcnp2  27009  jensen  27032  eupthvdres  30254  sspg  30747  ssps  30749  sspn  30755  hhsssh  31288  fnresin  32636  padct  32731  ffsrn  32740  resf1o  32741  indf1ofs  32851  gsumle  33101  symgcom  33103  cycpmconjvlem  33161  cycpmconjslem1  33174  nsgqusf1o  33444  ply1degltdimlem  33673  cnrrext  34011  eulerpartlemt  34373  subfacp1lem3  35187  subfacp1lem5  35189  cvmliftlem11  35300  poimirlem9  37636  dvun  42389  mapfzcons1  42728  eq0rabdioph  42787  eldioph4b  42822  diophren  42824  pwssplit4  43101  tfsconcatrev  43361  dvresntr  45933  sge0split  46424