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  27788  dfiop2  31006  idunop  31231  idcnop  31234  elunop2  31266  lnophm  31272  pmtridfv1  32254  pmtridfv2  32255  cycpmfv3  32274  islinds5  32480  ellspds  32481  evls1varpwval  32645  algextdeglem1  32772  qqhre  33000  subfacp1lem4  34174  subfacp1lem5  34175  cvmliftlem5  34280  bj-evalid  35957  idlaut  38967  idldil  38985  ltrnid  39006  idltrn  39021  ltrnideq  39046  tendoidcl  39640  tendo1ne0  39699  cdleml7  39853  dvalveclem  39896  dvhlveclem  39979  cdlemn8  40075  cdlemn11a  40078  rngunsnply  41915  fundcmpsurbijinjpreimafv  46075  fundcmpsurinjimaid  46079  isomgreqve  46493  isomushgr  46494  ushrisomgr  46509  idmgmhm  46558  funcrngcsetcALT  46897  funcringcsetcALTV2lem6  46939  funcringcsetcALTV2lem7  46940  funcringcsetcALTV2lem9  46942  funcringcsetclem6ALTV  46962  funcringcsetclem7ALTV  46963  funcringcsetclem9ALTV  46965  dflinc2  47091