Theorem fnresdm 6038

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 6027	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6028	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3690	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 5472	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 694	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1523   ⊆ wss 3607  dom cdm 5143   ↾ cres 5145  Rel wrel 5148   Fn wfn 5921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150  df-dm 5153  df-res 5155  df-fun 5928  df-fn 5929

This theorem is referenced by:  fnima  6048  fresin  6111  resasplit  6112  fresaunres2  6114  fvreseq1  6358  fnsnr  6472  fninfp  6481  fnsnsplit  6491  fsnunfv  6494  fsnunres  6495  fnsuppeq0  7368  mapunen  8170  fnfi  8279  canthp1lem2  9513  fseq1p1m1  12452  facnn  13102  fac0  13103  hashgval  13160  hashinf  13162  rlimres  14333  lo1res  14334  rlimresb  14340  isercolllem2  14440  isercoll  14442  ruclem4  15007  fsets  15938  sscres  16530  sscid  16531  gsumzres  18356  pwssplit1  19107  zzngim  19949  ptuncnv  21658  ptcmpfi  21664  tsmsres  21994  imasdsf1olem  22225  tmslem  22334  tmsxms  22338  imasf1oxms  22341  prdsxms  22382  tmsxps  22388  tmsxpsmopn  22389  isngp2  22448  tngngp2  22503  cnfldms  22626  cncms  23197  cnfldcusp  23199  mbfres2  23457  dvres  23720  dvres3a  23723  cpnres  23745  dvmptres3  23764  dvlip2  23803  dvgt0lem2  23811  dvne0  23819  rlimcnp2  24738  jensen  24760  eupthvdres  27213  sspg  27711  ssps  27713  sspn  27719  hhsssh  28254  fnresin  29558  padct  29625  ffsrn  29632  resf1o  29633  gsumle  29907  cnrrext  30182  indf1ofs  30216  eulerpartlemt  30561  subfacp1lem3  31290  subfacp1lem5  31292  cvmliftlem11  31403  poimirlem9  33548  mapfzcons1  37597  eq0rabdioph  37657  eldioph4b  37692  diophren  37694  pwssplit4  37976  dvresntr  40450  sge0split  40944