Theorem fvresi 7119

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   I cid 5518   ↾ cres 5626  ‘cfv 6492

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 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-res 5636  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fninfp  7120  fndifnfp  7122  fnnfpeq0  7124  f1ocnvfv1  7222  f1ocnvfv2  7223  fcof1  7233  fcofo  7234  isoid  7275  weniso  7300  iordsmo  8289  fipreima  9260  infxpenc  9930  dfac9  10049  fproddvdsd  16264  ndxarg  17125  idfu2  17804  idfu1  17806  idfucl  17807  cofurid  17817  funcestrcsetclem6  18070  funcestrcsetclem7  18071  funcestrcsetclem9  18073  funcsetcestrclem6  18085  funcsetcestrclem7  18086  funcsetcestrclem9  18088  yonedainv  18206  idmgmhm  18628  idmhm  18722  smndex1n0mnd  18839  idghm  19162  lactghmga  19336  symgga  19338  cayleylem2  19344  gsmsymgrfix  19359  gsmsymgreq  19363  pmtrfinv  19392  funcrngcsetcALT  20576  idlmhm  20995  islinds2  21770  lindsind2  21776  psdmplcl  22107  evl1vard  22283  evls1varpwval  22314  madetsumid  22407  mdetunilem7  22564  txkgen  23598  ustuqtop3  24189  iducn  24228  nmoid  24688  dvid  25877  mvth  25955  fta1blem  26134  qaa  26289  idmot  28611  dfiop2  31830  idunop  32055  idcnop  32058  elunop2  32090  lnophm  32096  fcobijfs2  32803  fzo0pmtrlast  33176  pmtridfv1  33179  pmtridfv2  33180  cycpmfv3  33199  islinds5  33450  ellspds  33451  vr1nz  33676  algextdeglem4  33879  2sqr3minply  33939  cos9thpiminplylem6  33946  qqhre  34179  subfacp1lem4  35379  subfacp1lem5  35380  cvmliftlem5  35485  bj-evalid  37283  idlaut  40378  idldil  40396  ltrnid  40417  idltrn  40432  ltrnideq  40457  tendoidcl  41051  tendo1ne0  41110  cdleml7  41264  dvalveclem  41307  dvhlveclem  41390  cdlemn8  41486  cdlemn11a  41489  rngunsnply  43432  fundcmpsurbijinjpreimafv  47674  fundcmpsurinjimaid  47678  grimidvtxedg  48152  gricushgr  48184  ushggricedg  48194  grlicref  48279  gpgprismgr4cycllem10  48371  grlimedgnedg  48398  funcringcsetcALTV2lem6  48562  funcringcsetcALTV2lem7  48563  funcringcsetcALTV2lem9  48565  funcringcsetclem6ALTV  48585  funcringcsetclem7ALTV  48586  funcringcsetclem9ALTV  48588  dflinc2  48677  tposideq  49154  imaidfu  49376  opf2  49672  oduoppcciso  49832