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

Theorem fvresi 7120
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 6862 . 2 (𝐵𝐴 → (( I ↾ 𝐴)‘𝐵) = ( I ‘𝐵))
2 fvi 6918 . 2 (𝐵𝐴 → ( I ‘𝐵) = 𝐵)
31, 2eqtrd 2773 1 (𝐵𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107   I cid 5531  cres 5636  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-res 5646  df-iota 6449  df-fun 6499  df-fv 6505
This theorem is referenced by:  fninfp  7121  fndifnfp  7123  fnnfpeq0  7125  f1ocnvfv1  7223  f1ocnvfv2  7224  fcof1  7234  fcofo  7235  isoid  7275  weniso  7300  iordsmo  8304  fipreima  9305  infxpenc  9959  dfac9  10077  fproddvdsd  16222  ndxarg  17073  idfu2  17769  idfu1  17771  idfucl  17772  cofurid  17782  funcestrcsetclem6  18038  funcestrcsetclem7  18039  funcestrcsetclem9  18041  funcsetcestrclem6  18053  funcsetcestrclem7  18054  funcsetcestrclem9  18056  yonedainv  18175  idmhm  18616  smndex1n0mnd  18727  idghm  19028  lactghmga  19192  symgga  19194  cayleylem2  19200  gsmsymgrfix  19215  gsmsymgreq  19219  pmtrfinv  19248  idlmhm  20517  islinds2  21235  lindsind2  21241  evl1vard  21719  madetsumid  21826  mdetunilem7  21983  txkgen  23019  ustuqtop3  23611  iducn  23651  nmoid  24122  dvid  25298  mvth  25372  fta1blem  25549  qaa  25699  idmot  27521  dfiop2  30737  idunop  30962  idcnop  30965  elunop2  30997  lnophm  31003  pmtridfv1  31993  pmtridfv2  31994  cycpmfv3  32013  islinds5  32203  ellspds  32204  evls1varpwval  32319  qqhre  32658  subfacp1lem4  33834  subfacp1lem5  33835  cvmliftlem5  33940  bj-evalid  35593  idlaut  38605  idldil  38623  ltrnid  38644  idltrn  38659  ltrnideq  38684  tendoidcl  39278  tendo1ne0  39337  cdleml7  39491  dvalveclem  39534  dvhlveclem  39617  cdlemn8  39713  cdlemn11a  39716  rngunsnply  41543  fundcmpsurbijinjpreimafv  45685  fundcmpsurinjimaid  45689  isomgreqve  46103  isomushgr  46104  ushrisomgr  46119  idmgmhm  46168  funcrngcsetcALT  46383  funcringcsetcALTV2lem6  46425  funcringcsetcALTV2lem7  46426  funcringcsetcALTV2lem9  46428  funcringcsetclem6ALTV  46448  funcringcsetclem7ALTV  46449  funcringcsetclem9ALTV  46451  dflinc2  46577
  Copyright terms: Public domain W3C validator