Theorem fnresdm 6669

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3948  dom cdm 5676   ↾ cres 5678  Rel wrel 5681   Fn wfn 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-dm 5686  df-res 5688  df-fun 6545  df-fn 6546

This theorem is referenced by:  fnima  6680  fresin  6760  resasplit  6761  fresaunres2  6763  fvreseq1  7040  fnsnr  7165  fninfp  7174  fnsnsplit  7184  fsnunfv  7187  fsnunres  7188  fnsuppeq0  8179  mapunen  9148  dif1enlem  9158  dif1enlemOLD  9159  fnfi  9183  canthp1lem2  10650  fseq1p1m1  13579  facnn  14239  fac0  14240  hashgval  14297  hashinf  14299  rlimres  15506  lo1res  15507  rlimresb  15513  isercolllem2  15616  isercoll  15618  ruclem4  16181  fsets  17106  sscres  17774  sscid  17775  gsumzres  19818  rnrhmsubrg  20495  pwssplit1  20814  zzngim  21327  ptuncnv  23531  ptcmpfi  23537  tsmsres  23868  imasdsf1olem  24099  tmslem  24210  tmslemOLD  24211  tmsxms  24215  imasf1oxms  24218  prdsxms  24259  tmsxps  24265  tmsxpsmopn  24266  isngp2  24326  tngngp2  24389  cnfldms  24512  cncms  25096  cnfldcusp  25098  mbfres2  25386  dvres  25652  dvres3a  25655  cpnres  25678  dvmptres3  25697  dvlip2  25736  dvgt0lem2  25744  dvne0  25752  rlimcnp2  26695  jensen  26717  eupthvdres  29743  sspg  30236  ssps  30238  sspn  30244  hhsssh  30777  fnresin  32105  padct  32199  ffsrn  32209  resf1o  32210  gsumle  32500  symgcom  32502  cycpmconjvlem  32558  cycpmconjslem1  32571  nsgqusf1o  32789  ply1degltdimlem  32983  cnrrext  33276  indf1ofs  33310  eulerpartlemt  33656  subfacp1lem3  34459  subfacp1lem5  34461  cvmliftlem11  34572  poimirlem9  36800  mapfzcons1  41757  eq0rabdioph  41816  eldioph4b  41851  diophren  41853  pwssplit4  42133  tfsconcatrev  42400  dvresntr  44933  sge0split  45424