Theorem fvresi 7177

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   I cid 5557   ↾ cres 5665  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-res 5675  df-iota 6496  df-fun 6542  df-fv 6548

This theorem is used by:  fninfp  7178  fndifnfp  7180  fnnfpeq0  7182  f1ocnvfv1  7283  f1ocnvfv2  7284  fcof1  7294  fcofo  7295  isoid  7336  weniso  7363  iordsmo  8350  fipreima  9322  infxpenc  10018  dfac9  10136  fproddvdsd  16417  ndxarg  17280  idfu2  17959  idfu1  17961  idfucl  17962  cofurid  17972  funcestrcsetclem6  18225  funcestrcsetclem7  18226  funcestrcsetclem9  18228  funcsetcestrclem6  18240  funcsetcestrclem7  18241  funcsetcestrclem9  18243  yonedainv  18361  idmgmhm  18793  idmhm  18892  smndex1n0mnd  19013  idghm  19347  lactghmga  19521  symgga  19523  cayleylem2  19529  gsmsymgrfix  19544  gsmsymgreq  19548  pmtrfinv  19577  funcrngcsetcALT  20792  idlmhm  21214  islinds2  22015  lindsind2  22021  psdmplcl  22377  evl1vard  22549  evls1varpwval  22580  madetsumid  22670  mdetunilem7  22827  txkgen  23862  ustuqtop3  24453  iducn  24492  nmoid  24952  dvid  26130  mvth  26204  fta1blem  26381  qaa  26537  idmot  28859  dfiop2  32178  idunop  32403  idcnop  32406  elunop2  32438  lnophm  32444  fcobijfs2  33139  fzo0pmtrlast  33478  pmtridfv1  33481  pmtridfv2  33482  cycpmfv3  33501  islinds5  33748  ellspds  33749  vr1nz  33949  algextdeglem4  34176  2sqr3minply  34236  cos9thpiminplylem6  34243  qqhre  34476  subfacp1lem4  35714  subfacp1lem5  35715  cvmliftlem5  35820  bj-evalid  37777  idlaut  40930  idldil  40948  ltrnid  40969  idltrn  40984  ltrnideq  41009  tendoidcl  41603  tendo1ne0  41662  cdleml7  41816  dvalveclem  41859  dvhlveclem  41942  cdlemn8  42038  cdlemn11a  42041  rngunsnply  43956  fundcmpsurbijinjpreimafv  48216  fundcmpsurinjimaid  48220  grimidvtxedg  48710  gricushgr  48742  ushggricedg  48752  grlicref  48837  gpgprismgr4cycllem10  48929  grlimedgnedg  48956  funcringcsetcALTV2lem6  49119  funcringcsetcALTV2lem7  49120  funcringcsetcALTV2lem9  49122  funcringcsetclem6ALTV  49142  funcringcsetclem7ALTV  49143  funcringcsetclem9ALTV  49145  dflinc2  49249  tposideq  49725  imaidfu  49947  opf2  50243  oduoppcciso  50403