MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnresdm Structured version   Visualization version   GIF version

Theorem fnresdm 6446
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
StepHypRef Expression
1 fnrel 6433 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
2 fndm 6434 . . 3 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3 eqimss 3998 . . 3 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
42, 3syl 17 . 2 (𝐹 Fn 𝐴 → dom 𝐹𝐴)
5 relssres 5871 . 2 ((Rel 𝐹 ∧ dom 𝐹𝐴) → (𝐹𝐴) = 𝐹)
61, 4, 5syl2anc 587 1 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wss 3908  dom cdm 5532  cres 5534  Rel wrel 5537   Fn wfn 6329
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-br 5043  df-opab 5105  df-xp 5538  df-rel 5539  df-dm 5542  df-res 5544  df-fun 6336  df-fn 6337
This theorem is referenced by:  fnima  6458  fresin  6528  resasplit  6529  fresaunres2  6531  fvreseq1  6791  fnsnr  6909  fninfp  6918  fnsnsplit  6928  fsnunfv  6931  fsnunres  6932  fnsuppeq0  7845  mapunen  8674  fnfi  8784  canthp1lem2  10064  fseq1p1m1  12976  facnn  13631  fac0  13632  hashgval  13689  hashinf  13691  rlimres  14906  lo1res  14907  rlimresb  14913  isercolllem2  15013  isercoll  15015  ruclem4  15578  fsets  16507  sscres  17084  sscid  17085  gsumzres  19020  rnrhmsubrg  19558  pwssplit1  19822  zzngim  20242  ptuncnv  22410  ptcmpfi  22416  tsmsres  22747  imasdsf1olem  22978  tmslem  23087  tmsxms  23091  imasf1oxms  23094  prdsxms  23135  tmsxps  23141  tmsxpsmopn  23142  isngp2  23201  tngngp2  23256  cnfldms  23379  cncms  23957  cnfldcusp  23959  mbfres2  24247  dvres  24512  dvres3a  24515  cpnres  24538  dvmptres3  24557  dvlip2  24596  dvgt0lem2  24604  dvne0  24612  rlimcnp2  25550  jensen  25572  eupthvdres  28018  sspg  28509  ssps  28511  sspn  28517  hhsssh  29050  fnresin  30379  padct  30465  ffsrn  30475  resf1o  30476  gsumle  30756  symgcom  30758  cycpmconjvlem  30814  cycpmconjslem1  30827  cnrrext  31325  indf1ofs  31359  eulerpartlemt  31703  subfacp1lem3  32503  subfacp1lem5  32505  cvmliftlem11  32616  poimirlem9  35024  mapfzcons1  39588  eq0rabdioph  39647  eldioph4b  39682  diophren  39684  pwssplit4  39963  dvresntr  42499  sge0split  42987
  Copyright terms: Public domain W3C validator