Theorem fvresi 7158

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

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143   I cid 5542   ↾ cres 5650  ‘cfv 6522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-res 5660  df-iota 6478  df-fun 6524  df-fv 6530

This theorem is referenced by:  fninfp  7159  fndifnfp  7161  fnnfpeq0  7163  f1ocnvfv1  7261  f1ocnvfv2  7262  fcof1  7272  fcofo  7273  isoid  7314  weniso  7339  iordsmo  8329  fipreima  9302  infxpenc  9975  dfac9  10094  fproddvdsd  16370  ndxarg  17233  idfu2  17912  idfu1  17914  idfucl  17915  cofurid  17925  funcestrcsetclem6  18178  funcestrcsetclem7  18179  funcestrcsetclem9  18181  funcsetcestrclem6  18193  funcsetcestrclem7  18194  funcsetcestrclem9  18196  yonedainv  18314  idmgmhm  18736  idmhm  18830  smndex1n0mnd  18950  idghm  19272  lactghmga  19446  symgga  19448  cayleylem2  19454  gsmsymgrfix  19469  gsmsymgreq  19473  pmtrfinv  19502  funcrngcsetcALT  20692  idlmhm  21109  islinds2  21866  lindsind2  21872  psdmplcl  22228  evl1vard  22401  evls1varpwval  22432  madetsumid  22522  mdetunilem7  22679  txkgen  23713  ustuqtop3  24304  iducn  24343  nmoid  24803  dvid  25981  mvth  26055  fta1blem  26232  qaa  26388  idmot  28707  dfiop2  31957  idunop  32182  idcnop  32185  elunop2  32217  lnophm  32223  fcobijfs2  32925  fzo0pmtrlast  33273  pmtridfv1  33276  pmtridfv2  33277  cycpmfv3  33296  islinds5  33554  ellspds  33555  vr1nz  33790  algextdeglem4  34018  2sqr3minply  34078  cos9thpiminplylem6  34085  qqhre  34318  subfacp1lem4  35534  subfacp1lem5  35535  cvmliftlem5  35640  bj-evalid  37567  idlaut  40721  idldil  40739  ltrnid  40760  idltrn  40775  ltrnideq  40800  tendoidcl  41394  tendo1ne0  41453  cdleml7  41607  dvalveclem  41650  dvhlveclem  41733  cdlemn8  41829  cdlemn11a  41832  rngunsnply  43747  fundcmpsurbijinjpreimafv  48014  fundcmpsurinjimaid  48018  grimidvtxedg  48508  gricushgr  48540  ushggricedg  48550  grlicref  48635  gpgprismgr4cycllem10  48727  grlimedgnedg  48754  funcringcsetcALTV2lem6  48918  funcringcsetcALTV2lem7  48919  funcringcsetcALTV2lem9  48921  funcringcsetclem6ALTV  48941  funcringcsetclem7ALTV  48942  funcringcsetclem9ALTV  48944  dflinc2  49033  tposideq  49510  imaidfu  49732  opf2  50028  oduoppcciso  50188