Theorem fvresi 7172

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   I cid 5549   ↾ cres 5657  ‘cfv 6533

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 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-res 5667  df-iota 6489  df-fun 6535  df-fv 6541

This theorem is used by:  fninfp  7173  fndifnfp  7175  fnnfpeq0  7177  f1ocnvfv1  7278  f1ocnvfv2  7279  fcof1  7289  fcofo  7290  isoid  7331  weniso  7358  iordsmo  8347  fipreima  9328  infxpenc  10024  dfac9  10142  fproddvdsd  16428  ndxarg  17291  idfu2  17970  idfu1  17972  idfucl  17973  cofurid  17983  funcestrcsetclem6  18236  funcestrcsetclem7  18237  funcestrcsetclem9  18239  funcsetcestrclem6  18251  funcsetcestrclem7  18252  funcsetcestrclem9  18254  yonedainv  18372  idmgmhm  18806  idmhm  18906  smndex1n0mnd  19027  idghm  19361  lactghmga  19535  symgga  19537  cayleylem2  19543  gsmsymgrfix  19558  gsmsymgreq  19562  pmtrfinv  19591  funcrngcsetcALT  20806  idlmhm  21228  islinds2  22029  lindsind2  22035  psdmplcl  22393  evl1vard  22565  evls1varpwval  22596  madetsumid  22686  mdetunilem7  22843  txkgen  23881  ustuqtop3  24472  iducn  24511  nmoid  24971  dvid  26148  mvth  26222  fta1blem  26399  idpfv  26438  qaa  26559  idmot  28882  dfiop2  32237  idunop  32462  idcnop  32465  elunop2  32497  lnophm  32503  fcobijfs2  33196  fzo0pmtrlast  33535  pmtridfv1  33538  pmtridfv2  33539  cycpmfv3  33558  islinds5  33805  ellspds  33806  vr1nz  34006  algextdeglem4  34233  2sqr3minply  34293  cos9thpiminplylem6  34300  qqhre  34533  subfacp1lem4  35765  subfacp1lem5  35766  cvmliftlem5  35871  bj-evalid  37829  idlaut  40972  idldil  40990  ltrnid  41011  idltrn  41026  ltrnideq  41051  tendoidcl  41645  tendo1ne0  41704  cdleml7  41858  dvalveclem  41901  dvhlveclem  41984  cdlemn8  42080  cdlemn11a  42083  rngunsnply  44013  fundcmpsurbijinjpreimafv  48310  fundcmpsurinjimaid  48314  grimidvtxedg  48804  gricushgr  48836  ushggricedg  48846  grlicref  48931  gpgprismgr4cycllem10  49023  grlimedgnedg  49050  funcringcsetcALTV2lem6  49213  funcringcsetcALTV2lem7  49214  funcringcsetcALTV2lem9  49216  funcringcsetclem6ALTV  49236  funcringcsetclem7ALTV  49237  funcringcsetclem9ALTV  49239  dflinc2  49343  tposideq  49817  imaidfu  50039  opf2  50335  oduoppcciso  50495