Theorem fvresi 7109

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   I cid 5513   ↾ cres 5621  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-res 5631  df-iota 6438  df-fun 6484  df-fv 6490

This theorem is referenced by:  fninfp  7110  fndifnfp  7112  fnnfpeq0  7114  f1ocnvfv1  7213  f1ocnvfv2  7214  fcof1  7224  fcofo  7225  isoid  7266  weniso  7291  iordsmo  8280  fipreima  9248  infxpenc  9912  dfac9  10031  fproddvdsd  16246  ndxarg  17107  idfu2  17785  idfu1  17787  idfucl  17788  cofurid  17798  funcestrcsetclem6  18051  funcestrcsetclem7  18052  funcestrcsetclem9  18054  funcsetcestrclem6  18066  funcsetcestrclem7  18067  funcsetcestrclem9  18069  yonedainv  18187  idmgmhm  18575  idmhm  18669  smndex1n0mnd  18786  idghm  19110  lactghmga  19284  symgga  19286  cayleylem2  19292  gsmsymgrfix  19307  gsmsymgreq  19311  pmtrfinv  19340  funcrngcsetcALT  20526  idlmhm  20945  islinds2  21720  lindsind2  21726  psdmplcl  22047  evl1vard  22222  evls1varpwval  22253  madetsumid  22346  mdetunilem7  22503  txkgen  23537  ustuqtop3  24129  iducn  24168  nmoid  24628  dvid  25817  mvth  25895  fta1blem  26074  qaa  26229  idmot  28482  dfiop2  31697  idunop  31922  idcnop  31925  elunop2  31957  lnophm  31963  fcobijfs2  32667  fzo0pmtrlast  33035  pmtridfv1  33038  pmtridfv2  33039  cycpmfv3  33058  islinds5  33305  ellspds  33306  vr1nz  33527  algextdeglem4  33693  2sqr3minply  33753  cos9thpiminplylem6  33760  qqhre  33993  subfacp1lem4  35166  subfacp1lem5  35167  cvmliftlem5  35272  bj-evalid  37060  idlaut  40085  idldil  40103  ltrnid  40124  idltrn  40139  ltrnideq  40164  tendoidcl  40758  tendo1ne0  40817  cdleml7  40971  dvalveclem  41014  dvhlveclem  41097  cdlemn8  41193  cdlemn11a  41196  rngunsnply  43152  fundcmpsurbijinjpreimafv  47401  fundcmpsurinjimaid  47405  grimidvtxedg  47879  gricushgr  47911  ushggricedg  47921  grlicref  48006  gpgprismgr4cycllem10  48098  grlimedgnedg  48125  funcringcsetcALTV2lem6  48289  funcringcsetcALTV2lem7  48290  funcringcsetcALTV2lem9  48292  funcringcsetclem6ALTV  48312  funcringcsetclem7ALTV  48313  funcringcsetclem9ALTV  48315  dflinc2  48405  tposideq  48882  imaidfu  49105  opf2  49401  oduoppcciso  49561