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 583	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1540   ⊆ 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 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  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  8182  mapunen  9152  dif1enlem  9162  dif1enlemOLD  9163  fnfi  9187  canthp1lem2  10654  fseq1p1m1  13582  facnn  14242  fac0  14243  hashgval  14300  hashinf  14302  rlimres  15509  lo1res  15510  rlimresb  15516  isercolllem2  15619  isercoll  15621  ruclem4  16184  fsets  17109  sscres  17777  sscid  17778  gsumzres  19825  rnrhmsubrg  20503  pwssplit1  20902  zzngim  21417  ptuncnv  23630  ptcmpfi  23636  tsmsres  23967  imasdsf1olem  24198  tmslem  24309  tmslemOLD  24310  tmsxms  24314  imasf1oxms  24317  prdsxms  24358  tmsxps  24364  tmsxpsmopn  24365  isngp2  24425  tngngp2  24488  cnfldms  24611  cncms  25202  cnfldcusp  25204  mbfres2  25493  dvres  25759  dvres3a  25762  cpnres  25786  dvmptres3  25807  dvlip2  25847  dvgt0lem2  25855  dvne0  25863  rlimcnp2  26811  jensen  26833  eupthvdres  29920  sspg  30413  ssps  30415  sspn  30421  hhsssh  30954  fnresin  32282  padct  32376  ffsrn  32386  resf1o  32387  gsumle  32677  symgcom  32679  cycpmconjvlem  32735  cycpmconjslem1  32748  nsgqusf1o  32966  ply1degltdimlem  33160  cnrrext  33453  indf1ofs  33487  eulerpartlemt  33833  subfacp1lem3  34636  subfacp1lem5  34638  cvmliftlem11  34749  poimirlem9  36960  mapfzcons1  41917  eq0rabdioph  41976  eldioph4b  42011  diophren  42013  pwssplit4  42293  tfsconcatrev  42560  dvresntr  45092  sge0split  45583