Theorem fvresi 6789

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

Syntax hints:   → wi 4   = wceq 1520   ∈ wcel 2079   I cid 5339   ↾ cres 5437  ‘cfv 6217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pr 5214

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-res 5447  df-iota 6181  df-fun 6219  df-fv 6225

This theorem is referenced by:  fninfp  6790  fndifnfp  6792  fnnfpeq0  6794  f1ocnvfv1  6889  f1ocnvfv2  6890  fcof1  6899  fcofo  6900  isoid  6936  weniso  6961  iordsmo  7837  fipreima  8666  infxpenc  9279  dfac9  9397  fproddvdsd  15505  ndxarg  16325  idfu2  16965  idfu1  16967  idfucl  16968  cofurid  16978  funcestrcsetclem6  17212  funcestrcsetclem7  17213  funcestrcsetclem9  17215  funcsetcestrclem6  17227  funcsetcestrclem7  17228  funcsetcestrclem9  17230  yonedainv  17348  idmhm  17771  idghm  18102  lactghmga  18251  symgga  18253  cayleylem2  18260  gsmsymgrfix  18275  gsmsymgreq  18279  pmtrfinv  18308  idlmhm  19491  evl1vard  20170  islinds2  20627  lindsind2  20633  madetsumid  20742  mdetunilem7  20899  txkgen  21932  ustuqtop3  22523  iducn  22563  nmoid  23022  dvid  24186  mvth  24260  fta1blem  24433  qaa  24583  idmot  25993  dfiop2  29209  idunop  29434  idcnop  29437  elunop2  29469  lnophm  29475  cycpmfv3  30368  islinds5  30535  ellspds  30536  pmtridfv1  30627  pmtridfv2  30628  qqhre  30834  subfacp1lem4  31994  subfacp1lem5  31995  cvmliftlem5  32100  bj-evalid  33911  idlaut  36713  idldil  36731  ltrnid  36752  idltrn  36767  ltrnideq  36792  tendoidcl  37386  tendo1ne0  37445  cdleml7  37599  dvalveclem  37642  dvhlveclem  37725  cdlemn8  37821  cdlemn11a  37824  rngunsnply  39209  isomgreqve  43426  isomushgr  43427  ushrisomgr  43442  idmgmhm  43491  funcrngcsetcALT  43702  funcringcsetcALTV2lem6  43744  funcringcsetcALTV2lem7  43745  funcringcsetcALTV2lem9  43747  funcringcsetclem6ALTV  43767  funcringcsetclem7ALTV  43768  funcringcsetclem9ALTV  43770  dflinc2  43899