Theorem fvresi 7193

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   I cid 5577   ↾ cres 5687  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-res 5697  df-iota 6514  df-fun 6563  df-fv 6569

This theorem is referenced by:  fninfp  7194  fndifnfp  7196  fnnfpeq0  7198  f1ocnvfv1  7296  f1ocnvfv2  7297  fcof1  7307  fcofo  7308  isoid  7349  weniso  7374  iordsmo  8397  fipreima  9398  infxpenc  10058  dfac9  10177  fproddvdsd  16372  ndxarg  17233  idfu2  17923  idfu1  17925  idfucl  17926  cofurid  17936  funcestrcsetclem6  18190  funcestrcsetclem7  18191  funcestrcsetclem9  18193  funcsetcestrclem6  18205  funcsetcestrclem7  18206  funcsetcestrclem9  18208  yonedainv  18326  idmgmhm  18714  idmhm  18808  smndex1n0mnd  18925  idghm  19249  lactghmga  19423  symgga  19425  cayleylem2  19431  gsmsymgrfix  19446  gsmsymgreq  19450  pmtrfinv  19479  funcrngcsetcALT  20641  idlmhm  21040  islinds2  21833  lindsind2  21839  psdmplcl  22166  evl1vard  22341  evls1varpwval  22372  madetsumid  22467  mdetunilem7  22624  txkgen  23660  ustuqtop3  24252  iducn  24292  nmoid  24763  dvid  25953  mvth  26031  fta1blem  26210  qaa  26365  idmot  28545  dfiop2  31772  idunop  31997  idcnop  32000  elunop2  32032  lnophm  32038  fzo0pmtrlast  33112  pmtridfv1  33115  pmtridfv2  33116  cycpmfv3  33135  islinds5  33395  ellspds  33396  algextdeglem4  33761  2sqr3minply  33791  qqhre  34021  subfacp1lem4  35188  subfacp1lem5  35189  cvmliftlem5  35294  bj-evalid  37077  idlaut  40098  idldil  40116  ltrnid  40137  idltrn  40152  ltrnideq  40177  tendoidcl  40771  tendo1ne0  40830  cdleml7  40984  dvalveclem  41027  dvhlveclem  41110  cdlemn8  41206  cdlemn11a  41209  rngunsnply  43181  fundcmpsurbijinjpreimafv  47394  fundcmpsurinjimaid  47398  grimidvtxedg  47876  gricushgr  47886  ushggricedg  47896  grlicref  47972  funcringcsetcALTV2lem6  48211  funcringcsetcALTV2lem7  48212  funcringcsetcALTV2lem9  48214  funcringcsetclem6ALTV  48234  funcringcsetclem7ALTV  48235  funcringcsetclem9ALTV  48237  dflinc2  48327  tposideq  48788  oduoppcciso  49170