Theorem fvresi 7192

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 6925	. 2 ⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = ( I ‘𝐵))
2		fvi 6984	. 2 ⊢ (𝐵 ∈ 𝐴 → ( I ‘𝐵) = 𝐵)
3	1, 2	eqtrd 2774	1 ⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   I cid 5581   ↾ cres 5690  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-res 5700  df-iota 6515  df-fun 6564  df-fv 6570

This theorem is referenced by:  fninfp  7193  fndifnfp  7195  fnnfpeq0  7197  f1ocnvfv1  7295  f1ocnvfv2  7296  fcof1  7306  fcofo  7307  isoid  7348  weniso  7373  iordsmo  8395  fipreima  9395  infxpenc  10055  dfac9  10174  fproddvdsd  16368  ndxarg  17229  idfu2  17928  idfu1  17930  idfucl  17931  cofurid  17941  funcestrcsetclem6  18200  funcestrcsetclem7  18201  funcestrcsetclem9  18203  funcsetcestrclem6  18215  funcsetcestrclem7  18216  funcsetcestrclem9  18218  yonedainv  18337  idmgmhm  18726  idmhm  18820  smndex1n0mnd  18937  idghm  19261  lactghmga  19437  symgga  19439  cayleylem2  19445  gsmsymgrfix  19460  gsmsymgreq  19464  pmtrfinv  19493  funcrngcsetcALT  20657  idlmhm  21057  islinds2  21850  lindsind2  21856  psdmplcl  22183  evl1vard  22356  evls1varpwval  22387  madetsumid  22482  mdetunilem7  22639  txkgen  23675  ustuqtop3  24267  iducn  24307  nmoid  24778  dvid  25967  mvth  26045  fta1blem  26224  qaa  26379  idmot  28559  dfiop2  31781  idunop  32006  idcnop  32009  elunop2  32041  lnophm  32047  fzo0pmtrlast  33094  pmtridfv1  33097  pmtridfv2  33098  cycpmfv3  33117  islinds5  33374  ellspds  33375  algextdeglem4  33725  2sqr3minply  33752  qqhre  33982  subfacp1lem4  35167  subfacp1lem5  35168  cvmliftlem5  35273  bj-evalid  37058  idlaut  40078  idldil  40096  ltrnid  40117  idltrn  40132  ltrnideq  40157  tendoidcl  40751  tendo1ne0  40810  cdleml7  40964  dvalveclem  41007  dvhlveclem  41090  cdlemn8  41186  cdlemn11a  41189  rngunsnply  43157  fundcmpsurbijinjpreimafv  47331  fundcmpsurinjimaid  47335  grimidvtxedg  47813  gricushgr  47823  ushggricedg  47833  grlicref  47907  funcringcsetcALTV2lem6  48138  funcringcsetcALTV2lem7  48139  funcringcsetcALTV2lem9  48141  funcringcsetclem6ALTV  48161  funcringcsetclem7ALTV  48162  funcringcsetclem9ALTV  48164  dflinc2  48255  oduoppcciso  48881