Theorem fvresi 7172

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   I cid 5556   ↾ cres 5664  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-res 5674  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is referenced by:  fninfp  7173  fndifnfp  7175  fnnfpeq0  7177  f1ocnvfv1  7275  f1ocnvfv2  7276  fcof1  7286  fcofo  7287  isoid  7328  weniso  7353  iordsmo  8344  fipreima  9315  infxpenc  10002  dfac9  10120  fproddvdsd  16393  ndxarg  17256  idfu2  17935  idfu1  17937  idfucl  17938  cofurid  17948  funcestrcsetclem6  18201  funcestrcsetclem7  18202  funcestrcsetclem9  18204  funcsetcestrclem6  18216  funcsetcestrclem7  18217  funcsetcestrclem9  18219  yonedainv  18337  idmgmhm  18759  idmhm  18853  smndex1n0mnd  18974  idghm  19301  lactghmga  19475  symgga  19477  cayleylem2  19483  gsmsymgrfix  19498  gsmsymgreq  19502  pmtrfinv  19531  funcrngcsetcALT  20726  idlmhm  21140  islinds2  21932  lindsind2  21938  psdmplcl  22294  evl1vard  22466  evls1varpwval  22497  madetsumid  22587  mdetunilem7  22744  txkgen  23778  ustuqtop3  24369  iducn  24408  nmoid  24868  dvid  26046  mvth  26120  fta1blem  26297  qaa  26453  idmot  28772  dfiop2  32046  idunop  32271  idcnop  32274  elunop2  32306  lnophm  32312  fcobijfs2  33008  fzo0pmtrlast  33353  pmtridfv1  33356  pmtridfv2  33357  cycpmfv3  33376  islinds5  33625  ellspds  33626  vr1nz  33828  algextdeglem4  34055  2sqr3minply  34115  cos9thpiminplylem6  34122  qqhre  34355  subfacp1lem4  35608  subfacp1lem5  35609  cvmliftlem5  35714  bj-evalid  37640  idlaut  40794  idldil  40812  ltrnid  40833  idltrn  40848  ltrnideq  40873  tendoidcl  41467  tendo1ne0  41526  cdleml7  41680  dvalveclem  41723  dvhlveclem  41806  cdlemn8  41902  cdlemn11a  41905  rngunsnply  43822  fundcmpsurbijinjpreimafv  48079  fundcmpsurinjimaid  48083  grimidvtxedg  48573  gricushgr  48605  ushggricedg  48615  grlicref  48700  gpgprismgr4cycllem10  48792  grlimedgnedg  48819  funcringcsetcALTV2lem6  48983  funcringcsetcALTV2lem7  48984  funcringcsetcALTV2lem9  48986  funcringcsetclem6ALTV  49006  funcringcsetclem7ALTV  49007  funcringcsetclem9ALTV  49009  dflinc2  49109  tposideq  49585  imaidfu  49807  opf2  50103  oduoppcciso  50263