Theorem fvresi 7119

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 2772	1 ⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   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 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 2709  ax-sep 5231  ax-pr 5368

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  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  7120  fndifnfp  7122  fnnfpeq0  7124  f1ocnvfv1  7222  f1ocnvfv2  7223  fcof1  7233  fcofo  7234  isoid  7275  weniso  7300  iordsmo  8288  fipreima  9259  infxpenc  9929  dfac9  10048  fproddvdsd  16293  ndxarg  17155  idfu2  17834  idfu1  17836  idfucl  17837  cofurid  17847  funcestrcsetclem6  18100  funcestrcsetclem7  18101  funcestrcsetclem9  18103  funcsetcestrclem6  18115  funcsetcestrclem7  18116  funcsetcestrclem9  18118  yonedainv  18236  idmgmhm  18658  idmhm  18752  smndex1n0mnd  18872  idghm  19195  lactghmga  19369  symgga  19371  cayleylem2  19377  gsmsymgrfix  19392  gsmsymgreq  19396  pmtrfinv  19425  funcrngcsetcALT  20607  idlmhm  21026  islinds2  21801  lindsind2  21807  psdmplcl  22137  evl1vard  22311  evls1varpwval  22342  madetsumid  22435  mdetunilem7  22592  txkgen  23626  ustuqtop3  24217  iducn  24256  nmoid  24716  dvid  25894  mvth  25969  fta1blem  26148  qaa  26302  idmot  28624  dfiop2  31844  idunop  32069  idcnop  32072  elunop2  32104  lnophm  32110  fcobijfs2  32815  fzo0pmtrlast  33173  pmtridfv1  33176  pmtridfv2  33177  cycpmfv3  33196  islinds5  33447  ellspds  33448  vr1nz  33673  algextdeglem4  33885  2sqr3minply  33945  cos9thpiminplylem6  33952  qqhre  34185  subfacp1lem4  35386  subfacp1lem5  35387  cvmliftlem5  35492  bj-evalid  37401  idlaut  40553  idldil  40571  ltrnid  40592  idltrn  40607  ltrnideq  40632  tendoidcl  41226  tendo1ne0  41285  cdleml7  41439  dvalveclem  41482  dvhlveclem  41565  cdlemn8  41661  cdlemn11a  41664  rngunsnply  43612  fundcmpsurbijinjpreimafv  47864  fundcmpsurinjimaid  47868  grimidvtxedg  48358  gricushgr  48390  ushggricedg  48400  grlicref  48485  gpgprismgr4cycllem10  48577  grlimedgnedg  48604  funcringcsetcALTV2lem6  48768  funcringcsetcALTV2lem7  48769  funcringcsetcALTV2lem9  48771  funcringcsetclem6ALTV  48791  funcringcsetclem7ALTV  48792  funcringcsetclem9ALTV  48794  dflinc2  48883  tposideq  49360  imaidfu  49582  opf2  49878  oduoppcciso  50038