Theorem fvresi 7147

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   I cid 5532   ↾ cres 5640  ‘cfv 6511

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-res 5650  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  fninfp  7148  fndifnfp  7150  fnnfpeq0  7152  f1ocnvfv1  7251  f1ocnvfv2  7252  fcof1  7262  fcofo  7263  isoid  7304  weniso  7329  iordsmo  8326  fipreima  9309  infxpenc  9971  dfac9  10090  fproddvdsd  16305  ndxarg  17166  idfu2  17840  idfu1  17842  idfucl  17843  cofurid  17853  funcestrcsetclem6  18106  funcestrcsetclem7  18107  funcestrcsetclem9  18109  funcsetcestrclem6  18121  funcsetcestrclem7  18122  funcsetcestrclem9  18124  yonedainv  18242  idmgmhm  18628  idmhm  18722  smndex1n0mnd  18839  idghm  19163  lactghmga  19335  symgga  19337  cayleylem2  19343  gsmsymgrfix  19358  gsmsymgreq  19362  pmtrfinv  19391  funcrngcsetcALT  20550  idlmhm  20948  islinds2  21722  lindsind2  21728  psdmplcl  22049  evl1vard  22224  evls1varpwval  22255  madetsumid  22348  mdetunilem7  22505  txkgen  23539  ustuqtop3  24131  iducn  24170  nmoid  24630  dvid  25819  mvth  25897  fta1blem  26076  qaa  26231  idmot  28464  dfiop2  31682  idunop  31907  idcnop  31910  elunop2  31942  lnophm  31948  fzo0pmtrlast  33049  pmtridfv1  33052  pmtridfv2  33053  cycpmfv3  33072  islinds5  33338  ellspds  33339  vr1nz  33559  algextdeglem4  33710  2sqr3minply  33770  cos9thpiminplylem6  33777  qqhre  34010  subfacp1lem4  35170  subfacp1lem5  35171  cvmliftlem5  35276  bj-evalid  37064  idlaut  40090  idldil  40108  ltrnid  40129  idltrn  40144  ltrnideq  40169  tendoidcl  40763  tendo1ne0  40822  cdleml7  40976  dvalveclem  41019  dvhlveclem  41102  cdlemn8  41198  cdlemn11a  41201  rngunsnply  43158  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjimaid  47412  grimidvtxedg  47885  gricushgr  47917  ushggricedg  47927  grlicref  48004  gpgprismgr4cycllem10  48094  funcringcsetcALTV2lem6  48283  funcringcsetcALTV2lem7  48284  funcringcsetcALTV2lem9  48286  funcringcsetclem6ALTV  48306  funcringcsetclem7ALTV  48307  funcringcsetclem9ALTV  48309  dflinc2  48399  tposideq  48876  imaidfu  49099  opf2  49395  oduoppcciso  49555