Theorem fvresi 7131

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   I cid 5528   ↾ cres 5636  ‘cfv 6502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-res 5646  df-iota 6458  df-fun 6504  df-fv 6510

This theorem is referenced by:  fninfp  7132  fndifnfp  7134  fnnfpeq0  7136  f1ocnvfv1  7234  f1ocnvfv2  7235  fcof1  7245  fcofo  7246  isoid  7287  weniso  7312  iordsmo  8301  fipreima  9272  infxpenc  9942  dfac9  10061  fproddvdsd  16276  ndxarg  17137  idfu2  17816  idfu1  17818  idfucl  17819  cofurid  17829  funcestrcsetclem6  18082  funcestrcsetclem7  18083  funcestrcsetclem9  18085  funcsetcestrclem6  18097  funcsetcestrclem7  18098  funcsetcestrclem9  18100  yonedainv  18218  idmgmhm  18640  idmhm  18734  smndex1n0mnd  18854  idghm  19177  lactghmga  19351  symgga  19353  cayleylem2  19359  gsmsymgrfix  19374  gsmsymgreq  19378  pmtrfinv  19407  funcrngcsetcALT  20591  idlmhm  21010  islinds2  21785  lindsind2  21791  psdmplcl  22122  evl1vard  22298  evls1varpwval  22329  madetsumid  22422  mdetunilem7  22579  txkgen  23613  ustuqtop3  24204  iducn  24243  nmoid  24703  dvid  25892  mvth  25970  fta1blem  26149  qaa  26304  idmot  28627  dfiop2  31847  idunop  32072  idcnop  32075  elunop2  32107  lnophm  32113  fcobijfs2  32818  fzo0pmtrlast  33192  pmtridfv1  33195  pmtridfv2  33196  cycpmfv3  33215  islinds5  33466  ellspds  33467  vr1nz  33692  algextdeglem4  33904  2sqr3minply  33964  cos9thpiminplylem6  33971  qqhre  34204  subfacp1lem4  35405  subfacp1lem5  35406  cvmliftlem5  35511  bj-evalid  37356  idlaut  40501  idldil  40519  ltrnid  40540  idltrn  40555  ltrnideq  40580  tendoidcl  41174  tendo1ne0  41233  cdleml7  41387  dvalveclem  41430  dvhlveclem  41513  cdlemn8  41609  cdlemn11a  41612  rngunsnply  43555  fundcmpsurbijinjpreimafv  47796  fundcmpsurinjimaid  47800  grimidvtxedg  48274  gricushgr  48306  ushggricedg  48316  grlicref  48401  gpgprismgr4cycllem10  48493  grlimedgnedg  48520  funcringcsetcALTV2lem6  48684  funcringcsetcALTV2lem7  48685  funcringcsetcALTV2lem9  48687  funcringcsetclem6ALTV  48707  funcringcsetclem7ALTV  48708  funcringcsetclem9ALTV  48710  dflinc2  48799  tposideq  49276  imaidfu  49498  opf2  49794  oduoppcciso  49954