Theorem fvresi 7207

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   I cid 5592   ↾ cres 5702  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-res 5712  df-iota 6525  df-fun 6575  df-fv 6581

This theorem is referenced by:  fninfp  7208  fndifnfp  7210  fnnfpeq0  7212  f1ocnvfv1  7312  f1ocnvfv2  7313  fcof1  7323  fcofo  7324  isoid  7365  weniso  7390  iordsmo  8413  fipreima  9428  infxpenc  10087  dfac9  10206  fproddvdsd  16383  ndxarg  17243  idfu2  17942  idfu1  17944  idfucl  17945  cofurid  17955  funcestrcsetclem6  18214  funcestrcsetclem7  18215  funcestrcsetclem9  18217  funcsetcestrclem6  18229  funcsetcestrclem7  18230  funcsetcestrclem9  18232  yonedainv  18351  idmgmhm  18739  idmhm  18830  smndex1n0mnd  18947  idghm  19271  lactghmga  19447  symgga  19449  cayleylem2  19455  gsmsymgrfix  19470  gsmsymgreq  19474  pmtrfinv  19503  funcrngcsetcALT  20663  idlmhm  21063  islinds2  21856  lindsind2  21862  psdmplcl  22189  evl1vard  22362  evls1varpwval  22393  madetsumid  22488  mdetunilem7  22645  txkgen  23681  ustuqtop3  24273  iducn  24313  nmoid  24784  dvid  25973  mvth  26051  fta1blem  26230  qaa  26383  idmot  28563  dfiop2  31785  idunop  32010  idcnop  32013  elunop2  32045  lnophm  32051  fzo0pmtrlast  33085  pmtridfv1  33088  pmtridfv2  33089  cycpmfv3  33108  islinds5  33360  ellspds  33361  algextdeglem4  33711  2sqr3minply  33738  qqhre  33966  subfacp1lem4  35151  subfacp1lem5  35152  cvmliftlem5  35257  bj-evalid  37042  idlaut  40053  idldil  40071  ltrnid  40092  idltrn  40107  ltrnideq  40132  tendoidcl  40726  tendo1ne0  40785  cdleml7  40939  dvalveclem  40982  dvhlveclem  41065  cdlemn8  41161  cdlemn11a  41164  rngunsnply  43130  fundcmpsurbijinjpreimafv  47281  fundcmpsurinjimaid  47285  grimidvtxedg  47760  gricushgr  47770  ushggricedg  47780  grlicref  47829  funcringcsetcALTV2lem6  48018  funcringcsetcALTV2lem7  48019  funcringcsetcALTV2lem9  48021  funcringcsetclem6ALTV  48041  funcringcsetclem7ALTV  48042  funcringcsetclem9ALTV  48044  dflinc2  48139