Theorem fnresdm 6637

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914  dom cdm 5638   ↾ cres 5640  Rel wrel 5643   Fn wfn 6506

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-dm 5648  df-res 5650  df-fun 6513  df-fn 6514

This theorem is referenced by:  fnima  6648  fresin  6729  resasplit  6730  fresaunres2  6732  fvreseq1  7011  fnsnr  7137  fninfp  7148  fnsnsplit  7158  fsnunfv  7161  fsnunres  7162  fnsuppeq0  8171  mapunen  9110  dif1enlem  9120  dif1enlemOLD  9121  fnfi  9142  canthp1lem2  10606  fseq1p1m1  13559  facnn  14240  fac0  14241  hashgval  14298  hashinf  14300  rlimres  15524  lo1res  15525  rlimresb  15531  isercolllem2  15632  isercoll  15634  ruclem4  16202  fsets  17139  sscres  17785  sscid  17786  gsumzres  19839  pwssplit1  20966  zzngim  21462  ptuncnv  23694  ptcmpfi  23700  tsmsres  24031  imasdsf1olem  24261  tmslem  24370  tmsxms  24374  imasf1oxms  24377  prdsxms  24418  tmsxps  24424  tmsxpsmopn  24425  isngp2  24485  tngngp2  24540  cnfldms  24663  cncms  25255  cnfldcusp  25257  mbfres2  25546  dvres  25812  dvres3a  25815  cpnres  25839  dvmptres3  25860  dvlip2  25900  dvgt0lem2  25908  dvne0  25916  rlimcnp2  26876  jensen  26899  eupthvdres  30164  sspg  30657  ssps  30659  sspn  30665  hhsssh  31198  fnresin  32550  padct  32643  ffsrn  32652  resf1o  32653  indf1ofs  32789  gsumle  33038  symgcom  33040  cycpmconjvlem  33098  cycpmconjslem1  33111  nsgqusf1o  33387  ply1degltdimlem  33618  cnrrext  34000  eulerpartlemt  34362  subfacp1lem3  35169  subfacp1lem5  35171  cvmliftlem11  35282  poimirlem9  37623  dvun  42347  mapfzcons1  42705  eq0rabdioph  42764  eldioph4b  42799  diophren  42801  pwssplit4  43078  tfsconcatrev  43337  dvresntr  45916  sge0split  46407  imaidfu2  49100