Theorem fvresi 7107

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   I cid 5508   ↾ cres 5616  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-res 5626  df-iota 6437  df-fun 6483  df-fv 6489

This theorem is referenced by:  fninfp  7108  fndifnfp  7110  fnnfpeq0  7112  f1ocnvfv1  7210  f1ocnvfv2  7211  fcof1  7221  fcofo  7222  isoid  7263  weniso  7288  iordsmo  8277  fipreima  9242  infxpenc  9909  dfac9  10028  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  18609  idmhm  18703  smndex1n0mnd  18820  idghm  19143  lactghmga  19317  symgga  19319  cayleylem2  19325  gsmsymgrfix  19340  gsmsymgreq  19344  pmtrfinv  19373  funcrngcsetcALT  20556  idlmhm  20975  islinds2  21750  lindsind2  21756  psdmplcl  22077  evl1vard  22252  evls1varpwval  22283  madetsumid  22376  mdetunilem7  22533  txkgen  23567  ustuqtop3  24158  iducn  24197  nmoid  24657  dvid  25846  mvth  25924  fta1blem  26103  qaa  26258  idmot  28515  dfiop2  31733  idunop  31958  idcnop  31961  elunop2  31993  lnophm  31999  fcobijfs2  32705  fzo0pmtrlast  33061  pmtridfv1  33064  pmtridfv2  33065  cycpmfv3  33084  islinds5  33332  ellspds  33333  vr1nz  33554  algextdeglem4  33733  2sqr3minply  33793  cos9thpiminplylem6  33800  qqhre  34033  subfacp1lem4  35227  subfacp1lem5  35228  cvmliftlem5  35333  bj-evalid  37120  idlaut  40205  idldil  40223  ltrnid  40244  idltrn  40259  ltrnideq  40284  tendoidcl  40878  tendo1ne0  40937  cdleml7  41091  dvalveclem  41134  dvhlveclem  41217  cdlemn8  41313  cdlemn11a  41316  rngunsnply  43272  fundcmpsurbijinjpreimafv  47517  fundcmpsurinjimaid  47521  grimidvtxedg  47995  gricushgr  48027  ushggricedg  48037  grlicref  48122  gpgprismgr4cycllem10  48214  grlimedgnedg  48241  funcringcsetcALTV2lem6  48405  funcringcsetcALTV2lem7  48406  funcringcsetcALTV2lem9  48408  funcringcsetclem6ALTV  48428  funcringcsetclem7ALTV  48429  funcringcsetclem9ALTV  48431  dflinc2  48521  tposideq  48998  imaidfu  49221  opf2  49517  oduoppcciso  49677