Theorem fvresi 7084

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105   I cid 5505   ↾ cres 5609  ‘cfv 6465

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-id 5506  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-res 5619  df-iota 6417  df-fun 6467  df-fv 6473

This theorem is referenced by:  fninfp  7085  fndifnfp  7087  fnnfpeq0  7089  f1ocnvfv1  7187  f1ocnvfv2  7188  fcof1  7198  fcofo  7199  isoid  7239  weniso  7264  iordsmo  8236  fipreima  9201  infxpenc  9853  dfac9  9971  fproddvdsd  16120  ndxarg  16971  idfu2  17667  idfu1  17669  idfucl  17670  cofurid  17680  funcestrcsetclem6  17936  funcestrcsetclem7  17937  funcestrcsetclem9  17939  funcsetcestrclem6  17951  funcsetcestrclem7  17952  funcsetcestrclem9  17954  yonedainv  18073  idmhm  18513  smndex1n0mnd  18624  idghm  18922  lactghmga  19086  symgga  19088  cayleylem2  19094  gsmsymgrfix  19109  gsmsymgreq  19113  pmtrfinv  19142  idlmhm  20383  islinds2  21100  lindsind2  21106  evl1vard  21583  madetsumid  21690  mdetunilem7  21847  txkgen  22883  ustuqtop3  23475  iducn  23515  nmoid  23986  dvid  25162  mvth  25236  fta1blem  25413  qaa  25563  idmot  27031  dfiop2  30247  idunop  30472  idcnop  30475  elunop2  30507  lnophm  30513  pmtridfv1  31493  pmtridfv2  31494  cycpmfv3  31513  islinds5  31698  ellspds  31699  qqhre  32106  subfacp1lem4  33280  subfacp1lem5  33281  cvmliftlem5  33386  bj-evalid  35324  idlaut  38336  idldil  38354  ltrnid  38375  idltrn  38390  ltrnideq  38415  tendoidcl  39009  tendo1ne0  39068  cdleml7  39222  dvalveclem  39265  dvhlveclem  39348  cdlemn8  39444  cdlemn11a  39447  rngunsnply  41220  fundcmpsurbijinjpreimafv  45129  fundcmpsurinjimaid  45133  isomgreqve  45547  isomushgr  45548  ushrisomgr  45563  idmgmhm  45612  funcrngcsetcALT  45827  funcringcsetcALTV2lem6  45869  funcringcsetcALTV2lem7  45870  funcringcsetcALTV2lem9  45872  funcringcsetclem6ALTV  45892  funcringcsetclem7ALTV  45893  funcringcsetclem9ALTV  45895  dflinc2  46021