Theorem fvresi 7171

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143   I cid 5555   ↾ cres 5663  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-res 5673  df-iota 6492  df-fun 6538  df-fv 6544

This theorem is referenced by:  fninfp  7172  fndifnfp  7174  fnnfpeq0  7176  f1ocnvfv1  7274  f1ocnvfv2  7275  fcof1  7285  fcofo  7286  isoid  7327  weniso  7352  iordsmo  8340  fipreima  9311  infxpenc  9998  dfac9  10116  fproddvdsd  16388  ndxarg  17251  idfu2  17930  idfu1  17932  idfucl  17933  cofurid  17943  funcestrcsetclem6  18196  funcestrcsetclem7  18197  funcestrcsetclem9  18199  funcsetcestrclem6  18211  funcsetcestrclem7  18212  funcsetcestrclem9  18214  yonedainv  18332  idmgmhm  18754  idmhm  18848  smndex1n0mnd  18969  idghm  19296  lactghmga  19470  symgga  19472  cayleylem2  19478  gsmsymgrfix  19493  gsmsymgreq  19497  pmtrfinv  19526  funcrngcsetcALT  20740  idlmhm  21162  islinds2  21963  lindsind2  21969  psdmplcl  22325  evl1vard  22497  evls1varpwval  22528  madetsumid  22618  mdetunilem7  22775  txkgen  23809  ustuqtop3  24400  iducn  24439  nmoid  24899  dvid  26077  mvth  26151  fta1blem  26328  qaa  26484  idmot  28806  dfiop2  32105  idunop  32330  idcnop  32333  elunop2  32365  lnophm  32371  fcobijfs2  33067  fzo0pmtrlast  33412  pmtridfv1  33415  pmtridfv2  33416  cycpmfv3  33435  islinds5  33682  ellspds  33683  vr1nz  33883  algextdeglem4  34110  2sqr3minply  34170  cos9thpiminplylem6  34177  qqhre  34410  subfacp1lem4  35675  subfacp1lem5  35676  cvmliftlem5  35781  bj-evalid  37738  idlaut  40890  idldil  40908  ltrnid  40929  idltrn  40944  ltrnideq  40969  tendoidcl  41563  tendo1ne0  41622  cdleml7  41776  dvalveclem  41819  dvhlveclem  41902  cdlemn8  41998  cdlemn11a  42001  rngunsnply  43916  fundcmpsurbijinjpreimafv  48176  fundcmpsurinjimaid  48180  grimidvtxedg  48670  gricushgr  48702  ushggricedg  48712  grlicref  48797  gpgprismgr4cycllem10  48889  grlimedgnedg  48916  funcringcsetcALTV2lem6  49080  funcringcsetcALTV2lem7  49081  funcringcsetcALTV2lem9  49083  funcringcsetclem6ALTV  49103  funcringcsetclem7ALTV  49104  funcringcsetclem9ALTV  49106  dflinc2  49210  tposideq  49686  imaidfu  49908  opf2  50204  oduoppcciso  50364