Theorem fvresi 7045

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   I cid 5488   ↾ cres 5591  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-res 5601  df-iota 6391  df-fun 6435  df-fv 6441

This theorem is referenced by:  fninfp  7046  fndifnfp  7048  fnnfpeq0  7050  f1ocnvfv1  7148  f1ocnvfv2  7149  fcof1  7159  fcofo  7160  isoid  7200  weniso  7225  iordsmo  8188  fipreima  9125  infxpenc  9774  dfac9  9892  fproddvdsd  16044  ndxarg  16897  idfu2  17593  idfu1  17595  idfucl  17596  cofurid  17606  funcestrcsetclem6  17862  funcestrcsetclem7  17863  funcestrcsetclem9  17865  funcsetcestrclem6  17877  funcsetcestrclem7  17878  funcsetcestrclem9  17880  yonedainv  17999  idmhm  18439  smndex1n0mnd  18551  idghm  18849  lactghmga  19013  symgga  19015  cayleylem2  19021  gsmsymgrfix  19036  gsmsymgreq  19040  pmtrfinv  19069  idlmhm  20303  islinds2  21020  lindsind2  21026  evl1vard  21503  madetsumid  21610  mdetunilem7  21767  txkgen  22803  ustuqtop3  23395  iducn  23435  nmoid  23906  dvid  25082  mvth  25156  fta1blem  25333  qaa  25483  idmot  26898  dfiop2  30115  idunop  30340  idcnop  30343  elunop2  30375  lnophm  30381  pmtridfv1  31362  pmtridfv2  31363  cycpmfv3  31382  islinds5  31563  ellspds  31564  qqhre  31970  subfacp1lem4  33145  subfacp1lem5  33146  cvmliftlem5  33251  bj-evalid  35247  idlaut  38110  idldil  38128  ltrnid  38149  idltrn  38164  ltrnideq  38189  tendoidcl  38783  tendo1ne0  38842  cdleml7  38996  dvalveclem  39039  dvhlveclem  39122  cdlemn8  39218  cdlemn11a  39221  rngunsnply  40998  fundcmpsurbijinjpreimafv  44859  fundcmpsurinjimaid  44863  isomgreqve  45277  isomushgr  45278  ushrisomgr  45293  idmgmhm  45342  funcrngcsetcALT  45557  funcringcsetcALTV2lem6  45599  funcringcsetcALTV2lem7  45600  funcringcsetcALTV2lem9  45602  funcringcsetclem6ALTV  45622  funcringcsetclem7ALTV  45623  funcringcsetclem9ALTV  45625  dflinc2  45751