Theorem fvresi 7117

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   I cid 5516   ↾ cres 5624  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-res 5634  df-iota 6446  df-fun 6492  df-fv 6498

This theorem is referenced by:  fninfp  7118  fndifnfp  7120  fnnfpeq0  7122  f1ocnvfv1  7220  f1ocnvfv2  7221  fcof1  7231  fcofo  7232  isoid  7273  weniso  7298  iordsmo  8287  fipreima  9256  infxpenc  9926  dfac9  10045  fproddvdsd  16260  ndxarg  17121  idfu2  17800  idfu1  17802  idfucl  17803  cofurid  17813  funcestrcsetclem6  18066  funcestrcsetclem7  18067  funcestrcsetclem9  18069  funcsetcestrclem6  18081  funcsetcestrclem7  18082  funcsetcestrclem9  18084  yonedainv  18202  idmgmhm  18624  idmhm  18718  smndex1n0mnd  18835  idghm  19158  lactghmga  19332  symgga  19334  cayleylem2  19340  gsmsymgrfix  19355  gsmsymgreq  19359  pmtrfinv  19388  funcrngcsetcALT  20572  idlmhm  20991  islinds2  21766  lindsind2  21772  psdmplcl  22103  evl1vard  22279  evls1varpwval  22310  madetsumid  22403  mdetunilem7  22560  txkgen  23594  ustuqtop3  24185  iducn  24224  nmoid  24684  dvid  25873  mvth  25951  fta1blem  26130  qaa  26285  idmot  28558  dfiop2  31777  idunop  32002  idcnop  32005  elunop2  32037  lnophm  32043  fcobijfs2  32750  fzo0pmtrlast  33123  pmtridfv1  33126  pmtridfv2  33127  cycpmfv3  33146  islinds5  33397  ellspds  33398  vr1nz  33623  algextdeglem4  33826  2sqr3minply  33886  cos9thpiminplylem6  33893  qqhre  34126  subfacp1lem4  35326  subfacp1lem5  35327  cvmliftlem5  35432  bj-evalid  37220  idlaut  40295  idldil  40313  ltrnid  40334  idltrn  40349  ltrnideq  40374  tendoidcl  40968  tendo1ne0  41027  cdleml7  41181  dvalveclem  41224  dvhlveclem  41307  cdlemn8  41403  cdlemn11a  41406  rngunsnply  43353  fundcmpsurbijinjpreimafv  47595  fundcmpsurinjimaid  47599  grimidvtxedg  48073  gricushgr  48105  ushggricedg  48115  grlicref  48200  gpgprismgr4cycllem10  48292  grlimedgnedg  48319  funcringcsetcALTV2lem6  48483  funcringcsetcALTV2lem7  48484  funcringcsetcALTV2lem9  48486  funcringcsetclem6ALTV  48506  funcringcsetclem7ALTV  48507  funcringcsetclem9ALTV  48509  dflinc2  48598  tposideq  49075  imaidfu  49297  opf2  49593  oduoppcciso  49753