Theorem fvresi 7167

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   I cid 5572   ↾ cres 5677  ‘cfv 6540

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-res 5687  df-iota 6492  df-fun 6542  df-fv 6548

This theorem is referenced by:  fninfp  7168  fndifnfp  7170  fnnfpeq0  7172  f1ocnvfv1  7270  f1ocnvfv2  7271  fcof1  7281  fcofo  7282  isoid  7322  weniso  7347  iordsmo  8353  fipreima  9354  infxpenc  10009  dfac9  10127  fproddvdsd  16274  ndxarg  17125  idfu2  17824  idfu1  17826  idfucl  17827  cofurid  17837  funcestrcsetclem6  18093  funcestrcsetclem7  18094  funcestrcsetclem9  18096  funcsetcestrclem6  18108  funcsetcestrclem7  18109  funcsetcestrclem9  18111  yonedainv  18230  idmhm  18677  smndex1n0mnd  18789  idghm  19101  lactghmga  19267  symgga  19269  cayleylem2  19275  gsmsymgrfix  19290  gsmsymgreq  19294  pmtrfinv  19323  idlmhm  20644  islinds2  21359  lindsind2  21365  evl1vard  21847  madetsumid  21954  mdetunilem7  22111  txkgen  23147  ustuqtop3  23739  iducn  23779  nmoid  24250  dvid  25426  mvth  25500  fta1blem  25677  qaa  25827  idmot  27777  dfiop2  30993  idunop  31218  idcnop  31221  elunop2  31253  lnophm  31259  pmtridfv1  32241  pmtridfv2  32242  cycpmfv3  32261  islinds5  32468  ellspds  32469  evls1varpwval  32633  algextdeglem1  32760  qqhre  32988  subfacp1lem4  34162  subfacp1lem5  34163  cvmliftlem5  34268  bj-evalid  35945  idlaut  38955  idldil  38973  ltrnid  38994  idltrn  39009  ltrnideq  39034  tendoidcl  39628  tendo1ne0  39687  cdleml7  39841  dvalveclem  39884  dvhlveclem  39967  cdlemn8  40063  cdlemn11a  40066  rngunsnply  41900  fundcmpsurbijinjpreimafv  46061  fundcmpsurinjimaid  46065  isomgreqve  46479  isomushgr  46480  ushrisomgr  46495  idmgmhm  46544  funcrngcsetcALT  46850  funcringcsetcALTV2lem6  46892  funcringcsetcALTV2lem7  46893  funcringcsetcALTV2lem9  46895  funcringcsetclem6ALTV  46915  funcringcsetclem7ALTV  46916  funcringcsetclem9ALTV  46918  dflinc2  47044