Theorem fvresi 7027

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   I cid 5479   ↾ cres 5582  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-res 5592  df-iota 6376  df-fun 6420  df-fv 6426

This theorem is referenced by:  fninfp  7028  fndifnfp  7030  fnnfpeq0  7032  f1ocnvfv1  7129  f1ocnvfv2  7130  fcof1  7139  fcofo  7140  isoid  7180  weniso  7205  iordsmo  8159  fipreima  9055  infxpenc  9705  dfac9  9823  fproddvdsd  15972  ndxarg  16825  idfu2  17509  idfu1  17511  idfucl  17512  cofurid  17522  funcestrcsetclem6  17778  funcestrcsetclem7  17779  funcestrcsetclem9  17781  funcsetcestrclem6  17793  funcsetcestrclem7  17794  funcsetcestrclem9  17796  yonedainv  17915  idmhm  18354  smndex1n0mnd  18466  idghm  18764  lactghmga  18928  symgga  18930  cayleylem2  18936  gsmsymgrfix  18951  gsmsymgreq  18955  pmtrfinv  18984  idlmhm  20218  islinds2  20930  lindsind2  20936  evl1vard  21413  madetsumid  21518  mdetunilem7  21675  txkgen  22711  ustuqtop3  23303  iducn  23343  nmoid  23812  dvid  24987  mvth  25061  fta1blem  25238  qaa  25388  idmot  26802  dfiop2  30016  idunop  30241  idcnop  30244  elunop2  30276  lnophm  30282  pmtridfv1  31264  pmtridfv2  31265  cycpmfv3  31284  islinds5  31465  ellspds  31466  qqhre  31870  subfacp1lem4  33045  subfacp1lem5  33046  cvmliftlem5  33151  bj-evalid  35174  idlaut  38037  idldil  38055  ltrnid  38076  idltrn  38091  ltrnideq  38116  tendoidcl  38710  tendo1ne0  38769  cdleml7  38923  dvalveclem  38966  dvhlveclem  39049  cdlemn8  39145  cdlemn11a  39148  rngunsnply  40914  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjimaid  44751  isomgreqve  45165  isomushgr  45166  ushrisomgr  45181  idmgmhm  45230  funcrngcsetcALT  45445  funcringcsetcALTV2lem6  45487  funcringcsetcALTV2lem7  45488  funcringcsetcALTV2lem9  45490  funcringcsetclem6ALTV  45510  funcringcsetclem7ALTV  45511  funcringcsetclem9ALTV  45513  dflinc2  45639