Theorem fvresi 7171

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   I cid 5574   ↾ cres 5679  ‘cfv 6544

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-res 5689  df-iota 6496  df-fun 6546  df-fv 6552

This theorem is referenced by:  fninfp  7172  fndifnfp  7174  fnnfpeq0  7176  f1ocnvfv1  7274  f1ocnvfv2  7275  fcof1  7285  fcofo  7286  isoid  7326  weniso  7351  iordsmo  8357  fipreima  9358  infxpenc  10013  dfac9  10131  fproddvdsd  16278  ndxarg  17129  idfu2  17828  idfu1  17830  idfucl  17831  cofurid  17841  funcestrcsetclem6  18097  funcestrcsetclem7  18098  funcestrcsetclem9  18100  funcsetcestrclem6  18112  funcsetcestrclem7  18113  funcsetcestrclem9  18115  yonedainv  18234  idmhm  18681  smndex1n0mnd  18793  idghm  19107  lactghmga  19273  symgga  19275  cayleylem2  19281  gsmsymgrfix  19296  gsmsymgreq  19300  pmtrfinv  19329  idlmhm  20652  islinds2  21368  lindsind2  21374  evl1vard  21856  madetsumid  21963  mdetunilem7  22120  txkgen  23156  ustuqtop3  23748  iducn  23788  nmoid  24259  dvid  25435  mvth  25509  fta1blem  25686  qaa  25836  idmot  27819  dfiop2  31037  idunop  31262  idcnop  31265  elunop2  31297  lnophm  31303  pmtridfv1  32285  pmtridfv2  32286  cycpmfv3  32305  islinds5  32511  ellspds  32512  evls1varpwval  32676  algextdeglem1  32803  qqhre  33031  subfacp1lem4  34205  subfacp1lem5  34206  cvmliftlem5  34311  bj-evalid  36005  idlaut  39015  idldil  39033  ltrnid  39054  idltrn  39069  ltrnideq  39094  tendoidcl  39688  tendo1ne0  39747  cdleml7  39901  dvalveclem  39944  dvhlveclem  40027  cdlemn8  40123  cdlemn11a  40126  rngunsnply  41963  fundcmpsurbijinjpreimafv  46123  fundcmpsurinjimaid  46127  isomgreqve  46541  isomushgr  46542  ushrisomgr  46557  idmgmhm  46606  funcrngcsetcALT  46945  funcringcsetcALTV2lem6  46987  funcringcsetcALTV2lem7  46988  funcringcsetcALTV2lem9  46990  funcringcsetclem6ALTV  47010  funcringcsetclem7ALTV  47011  funcringcsetclem9ALTV  47013  dflinc2  47139