Theorem fvresi 7118

Description: The value of a restricted identity function. (Contributed by NM, 19-May-2004.)

Assertion

Ref	Expression
fvresi	⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)

Proof of Theorem fvresi

Step	Hyp	Ref	Expression
1		fvres 6847	. 2 ⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = ( I ‘𝐵))
2		fvi 6904	. 2 ⊢ (𝐵 ∈ 𝐴 → ( I ‘𝐵) = 𝐵)
3	1, 2	eqtrd 2774	1 ⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   I cid 5513   ↾ cres 5621  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-pr 5363

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-res 5631  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fninfp  7119  fndifnfp  7121  fnnfpeq0  7123  f1ocnvfv1  7221  f1ocnvfv2  7222  fcof1  7232  fcofo  7233  isoid  7274  weniso  7299  iordsmo  8288  fipreima  9259  infxpenc  9932  dfac9  10051  fproddvdsd  16296  ndxarg  17158  idfu2  17837  idfu1  17839  idfucl  17840  cofurid  17850  funcestrcsetclem6  18103  funcestrcsetclem7  18104  funcestrcsetclem9  18106  funcsetcestrclem6  18118  funcsetcestrclem7  18119  funcsetcestrclem9  18121  yonedainv  18239  idmgmhm  18661  idmhm  18755  smndex1n0mnd  18875  idghm  19198  lactghmga  19372  symgga  19374  cayleylem2  19380  gsmsymgrfix  19395  gsmsymgreq  19399  pmtrfinv  19428  funcrngcsetcALT  20614  idlmhm  21032  islinds2  21789  lindsind2  21795  psdmplcl  22151  evl1vard  22324  evls1varpwval  22355  madetsumid  22445  mdetunilem7  22602  txkgen  23636  ustuqtop3  24227  iducn  24266  nmoid  24726  dvid  25904  mvth  25978  fta1blem  26155  qaa  26308  idmot  28624  dfiop2  31843  idunop  32068  idcnop  32071  elunop2  32103  lnophm  32109  fcobijfs2  32815  fzo0pmtrlast  33174  pmtridfv1  33177  pmtridfv2  33178  cycpmfv3  33197  islinds5  33451  ellspds  33452  vr1nz  33685  algextdeglem4  33913  2sqr3minply  33973  cos9thpiminplylem6  33980  qqhre  34213  subfacp1lem4  35420  subfacp1lem5  35421  cvmliftlem5  35526  bj-evalid  37443  idlaut  40597  idldil  40615  ltrnid  40636  idltrn  40651  ltrnideq  40676  tendoidcl  41270  tendo1ne0  41329  cdleml7  41483  dvalveclem  41526  dvhlveclem  41609  cdlemn8  41705  cdlemn11a  41708  rngunsnply  43623  fundcmpsurbijinjpreimafv  47890  fundcmpsurinjimaid  47894  grimidvtxedg  48384  gricushgr  48416  ushggricedg  48426  grlicref  48511  gpgprismgr4cycllem10  48603  grlimedgnedg  48630  funcringcsetcALTV2lem6  48794  funcringcsetcALTV2lem7  48795  funcringcsetcALTV2lem9  48797  funcringcsetclem6ALTV  48817  funcringcsetclem7ALTV  48818  funcringcsetclem9ALTV  48820  dflinc2  48909  tposideq  49386  imaidfu  49608  opf2  49904  oduoppcciso  50064