Theorem fvresi 7128

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   I cid 5525   ↾ cres 5633  ‘cfv 6498

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-res 5643  df-iota 6454  df-fun 6500  df-fv 6506

This theorem is referenced by:  fninfp  7129  fndifnfp  7131  fnnfpeq0  7133  f1ocnvfv1  7231  f1ocnvfv2  7232  fcof1  7242  fcofo  7243  isoid  7284  weniso  7309  iordsmo  8297  fipreima  9268  infxpenc  9940  dfac9  10059  fproddvdsd  16304  ndxarg  17166  idfu2  17845  idfu1  17847  idfucl  17848  cofurid  17858  funcestrcsetclem6  18111  funcestrcsetclem7  18112  funcestrcsetclem9  18114  funcsetcestrclem6  18126  funcsetcestrclem7  18127  funcsetcestrclem9  18129  yonedainv  18247  idmgmhm  18669  idmhm  18763  smndex1n0mnd  18883  idghm  19206  lactghmga  19380  symgga  19382  cayleylem2  19388  gsmsymgrfix  19403  gsmsymgreq  19407  pmtrfinv  19436  funcrngcsetcALT  20618  idlmhm  21036  islinds2  21793  lindsind2  21799  psdmplcl  22128  evl1vard  22302  evls1varpwval  22333  madetsumid  22426  mdetunilem7  22583  txkgen  23617  ustuqtop3  24208  iducn  24247  nmoid  24707  dvid  25885  mvth  25959  fta1blem  26136  qaa  26289  idmot  28605  dfiop2  31824  idunop  32049  idcnop  32052  elunop2  32084  lnophm  32090  fcobijfs2  32795  fzo0pmtrlast  33153  pmtridfv1  33156  pmtridfv2  33157  cycpmfv3  33176  islinds5  33427  ellspds  33428  vr1nz  33653  algextdeglem4  33864  2sqr3minply  33924  cos9thpiminplylem6  33931  qqhre  34164  subfacp1lem4  35365  subfacp1lem5  35366  cvmliftlem5  35471  bj-evalid  37388  idlaut  40542  idldil  40560  ltrnid  40581  idltrn  40596  ltrnideq  40621  tendoidcl  41215  tendo1ne0  41274  cdleml7  41428  dvalveclem  41471  dvhlveclem  41554  cdlemn8  41650  cdlemn11a  41653  rngunsnply  43597  fundcmpsurbijinjpreimafv  47867  fundcmpsurinjimaid  47871  grimidvtxedg  48361  gricushgr  48393  ushggricedg  48403  grlicref  48488  gpgprismgr4cycllem10  48580  grlimedgnedg  48607  funcringcsetcALTV2lem6  48771  funcringcsetcALTV2lem7  48772  funcringcsetcALTV2lem9  48774  funcringcsetclem6ALTV  48794  funcringcsetclem7ALTV  48795  funcringcsetclem9ALTV  48797  dflinc2  48886  tposideq  49363  imaidfu  49585  opf2  49881  oduoppcciso  50041