MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvresi Structured version   Visualization version   GIF version

Theorem fvresi 6667
Description: The value of a restricted identity function. (Contributed by NM, 19-May-2004.)
Assertion
Ref Expression
fvresi (𝐵𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)

Proof of Theorem fvresi
StepHypRef Expression
1 fvres 6430 . 2 (𝐵𝐴 → (( I ↾ 𝐴)‘𝐵) = ( I ‘𝐵))
2 fvi 6479 . 2 (𝐵𝐴 → ( I ‘𝐵) = 𝐵)
31, 2eqtrd 2847 1 (𝐵𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2157   I cid 5225  cres 5320  cfv 6104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pr 5103
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-res 5330  df-iota 6067  df-fun 6106  df-fv 6112
This theorem is referenced by:  fninfp  6668  fndifnfp  6670  fnnfpeq0  6672  f1ocnvfv1  6759  f1ocnvfv2  6760  fcof1  6769  fcofo  6770  isoid  6806  weniso  6831  iordsmo  7693  fipreima  8514  infxpenc  9127  dfac9  9246  fproddvdsd  15282  ndxarg  16096  idfu2  16745  idfu1  16747  idfucl  16748  cofurid  16758  funcestrcsetclem6  16993  funcestrcsetclem7  16994  funcestrcsetclem9  16996  funcsetcestrclem6  17008  funcsetcestrclem7  17009  funcsetcestrclem9  17011  yonedainv  17129  idmhm  17552  idghm  17880  lactghmga  18028  symgga  18030  cayleylem2  18037  gsmsymgrfix  18052  gsmsymgreq  18056  pmtrfinv  18085  idlmhm  19251  evl1vard  19912  islinds2  20366  lindsind2  20372  madetsumid  20482  mdetunilem7  20639  txkgen  21673  ustuqtop3  22264  iducn  22304  nmoid  22763  dvid  23901  mvth  23975  fta1blem  24148  qaa  24298  idmot  25652  dfiop2  28946  idunop  29171  idcnop  29174  elunop2  29206  lnophm  29212  pmtridfv1  30188  pmtridfv2  30189  qqhre  30395  subfacp1lem4  31493  subfacp1lem5  31494  cvmliftlem5  31599  bj-evalid  33341  idlaut  35878  idldil  35896  ltrnid  35917  idltrn  35932  ltrnideq  35957  tendoidcl  36551  tendo1ne0  36610  cdleml7  36764  dvalveclem  36807  dvhlveclem  36890  cdlemn8  36986  cdlemn11a  36989  rngunsnply  38245  idmgmhm  42357  funcrngcsetcALT  42568  funcringcsetcALTV2lem6  42610  funcringcsetcALTV2lem7  42611  funcringcsetcALTV2lem9  42613  funcringcsetclem6ALTV  42633  funcringcsetclem7ALTV  42634  funcringcsetclem9ALTV  42636  dflinc2  42768
  Copyright terms: Public domain W3C validator