Theorem fvresi 7150

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   I cid 5535   ↾ cres 5643  ‘cfv 6514

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-res 5653  df-iota 6467  df-fun 6516  df-fv 6522

This theorem is referenced by:  fninfp  7151  fndifnfp  7153  fnnfpeq0  7155  f1ocnvfv1  7254  f1ocnvfv2  7255  fcof1  7265  fcofo  7266  isoid  7307  weniso  7332  iordsmo  8329  fipreima  9316  infxpenc  9978  dfac9  10097  fproddvdsd  16312  ndxarg  17173  idfu2  17847  idfu1  17849  idfucl  17850  cofurid  17860  funcestrcsetclem6  18113  funcestrcsetclem7  18114  funcestrcsetclem9  18116  funcsetcestrclem6  18128  funcsetcestrclem7  18129  funcsetcestrclem9  18131  yonedainv  18249  idmgmhm  18635  idmhm  18729  smndex1n0mnd  18846  idghm  19170  lactghmga  19342  symgga  19344  cayleylem2  19350  gsmsymgrfix  19365  gsmsymgreq  19369  pmtrfinv  19398  funcrngcsetcALT  20557  idlmhm  20955  islinds2  21729  lindsind2  21735  psdmplcl  22056  evl1vard  22231  evls1varpwval  22262  madetsumid  22355  mdetunilem7  22512  txkgen  23546  ustuqtop3  24138  iducn  24177  nmoid  24637  dvid  25826  mvth  25904  fta1blem  26083  qaa  26238  idmot  28471  dfiop2  31689  idunop  31914  idcnop  31917  elunop2  31949  lnophm  31955  fzo0pmtrlast  33056  pmtridfv1  33059  pmtridfv2  33060  cycpmfv3  33079  islinds5  33345  ellspds  33346  vr1nz  33566  algextdeglem4  33717  2sqr3minply  33777  cos9thpiminplylem6  33784  qqhre  34017  subfacp1lem4  35177  subfacp1lem5  35178  cvmliftlem5  35283  bj-evalid  37071  idlaut  40097  idldil  40115  ltrnid  40136  idltrn  40151  ltrnideq  40176  tendoidcl  40770  tendo1ne0  40829  cdleml7  40983  dvalveclem  41026  dvhlveclem  41109  cdlemn8  41205  cdlemn11a  41208  rngunsnply  43165  fundcmpsurbijinjpreimafv  47412  fundcmpsurinjimaid  47416  grimidvtxedg  47889  gricushgr  47921  ushggricedg  47931  grlicref  48008  gpgprismgr4cycllem10  48098  funcringcsetcALTV2lem6  48287  funcringcsetcALTV2lem7  48288  funcringcsetcALTV2lem9  48290  funcringcsetclem6ALTV  48310  funcringcsetclem7ALTV  48311  funcringcsetclem9ALTV  48313  dflinc2  48403  tposideq  48880  imaidfu  49103  opf2  49399  oduoppcciso  49559