Theorem fvresi 7178

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   I cid 5544   ↾ cres 5652  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-res 5662  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is used by:  fninfp  7179  fndifnfp  7181  fnnfpeq0  7183  f1ocnvfv1  7284  f1ocnvfv2  7285  fcof1  7295  fcofo  7296  isoid  7337  weniso  7364  iordsmo  8365  fipreima  9347  infxpenc  10097  dfac9  10215  fproddvdsd  16505  ndxarg  17374  idfu2  18053  idfu1  18055  idfucl  18056  cofurid  18066  funcestrcsetclem6  18319  funcestrcsetclem7  18320  funcestrcsetclem9  18322  funcsetcestrclem6  18334  funcsetcestrclem7  18335  funcsetcestrclem9  18337  yonedainv  18455  idmgmhm  18890  idmhm  18990  smndex1n0mnd  19111  idghm  19445  lactghmga  19619  symgga  19621  cayleylem2  19627  gsmsymgrfix  19642  gsmsymgreq  19646  pmtrfinv  19675  funcrngcsetcALT  20893  idlmhm  21316  islinds2  22119  lindsind2  22125  psdmplcl  22483  evl1vard  22655  evls1varpwval  22686  madetsumid  22776  mdetunilem7  22933  txkgen  23971  ustuqtop3  24562  iducn  24601  nmoid  25061  dvid  26238  mvth  26312  fta1blem  26489  idpfv  26528  qaa  26647  idmot  29000  dfiop2  32355  idunop  32580  idcnop  32583  elunop2  32615  lnophm  32621  fcobijfs2  33314  fzo0pmtrlast  33653  pmtridfv1  33656  pmtridfv2  33657  cycpmfv3  33676  islinds5  33923  ellspds  33924  vr1nz  34125  algextdeglem4  34352  2sqr3minply  34412  cos9thpiminplylem6  34419  qqhre  34652  subfacp1lem4  35948  subfacp1lem5  35949  cvmliftlem5  36054  bj-evalid  37997  idlaut  41154  idldil  41172  ltrnid  41193  idltrn  41208  ltrnideq  41233  tendoidcl  41827  tendo1ne0  41886  cdleml7  42040  dvalveclem  42083  dvhlveclem  42166  cdlemn8  42262  cdlemn11a  42265  rngunsnply  44171  fundcmpsurbijinjpreimafv  48489  fundcmpsurinjimaid  48493  grimidvtxedg  48983  gricushgr  49015  ushggricedg  49025  grlicref  49110  gpgprismgr4cycllem10  49202  grlimedgnedg  49229  funcringcsetcALTV2lem6  49392  funcringcsetcALTV2lem7  49393  funcringcsetcALTV2lem9  49395  funcringcsetclem6ALTV  49415  funcringcsetclem7ALTV  49416  funcringcsetclem9ALTV  49418  dflinc2  49522  tposideq  49996  imaidfu  50218  opf2  50514  oduoppcciso  50674