Theorem fvresi 7123

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   I cid 5520   ↾ cres 5628  ‘cfv 6494

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 5232  ax-pr 5372

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-res 5638  df-iota 6450  df-fun 6496  df-fv 6502

This theorem is referenced by:  fninfp  7124  fndifnfp  7126  fnnfpeq0  7128  f1ocnvfv1  7226  f1ocnvfv2  7227  fcof1  7237  fcofo  7238  isoid  7279  weniso  7304  iordsmo  8292  fipreima  9263  infxpenc  9935  dfac9  10054  fproddvdsd  16299  ndxarg  17161  idfu2  17840  idfu1  17842  idfucl  17843  cofurid  17853  funcestrcsetclem6  18106  funcestrcsetclem7  18107  funcestrcsetclem9  18109  funcsetcestrclem6  18121  funcsetcestrclem7  18122  funcsetcestrclem9  18124  yonedainv  18242  idmgmhm  18664  idmhm  18758  smndex1n0mnd  18878  idghm  19201  lactghmga  19375  symgga  19377  cayleylem2  19383  gsmsymgrfix  19398  gsmsymgreq  19402  pmtrfinv  19431  funcrngcsetcALT  20613  idlmhm  21032  islinds2  21807  lindsind2  21813  psdmplcl  22142  evl1vard  22316  evls1varpwval  22347  madetsumid  22440  mdetunilem7  22597  txkgen  23631  ustuqtop3  24222  iducn  24261  nmoid  24721  dvid  25899  mvth  25973  fta1blem  26150  qaa  26304  idmot  28623  dfiop2  31843  idunop  32068  idcnop  32071  elunop2  32103  lnophm  32109  fcobijfs2  32814  fzo0pmtrlast  33172  pmtridfv1  33175  pmtridfv2  33176  cycpmfv3  33195  islinds5  33446  ellspds  33447  vr1nz  33672  algextdeglem4  33884  2sqr3minply  33944  cos9thpiminplylem6  33951  qqhre  34184  subfacp1lem4  35385  subfacp1lem5  35386  cvmliftlem5  35491  bj-evalid  37408  idlaut  40560  idldil  40578  ltrnid  40599  idltrn  40614  ltrnideq  40639  tendoidcl  41233  tendo1ne0  41292  cdleml7  41446  dvalveclem  41489  dvhlveclem  41572  cdlemn8  41668  cdlemn11a  41671  rngunsnply  43619  fundcmpsurbijinjpreimafv  47883  fundcmpsurinjimaid  47887  grimidvtxedg  48377  gricushgr  48409  ushggricedg  48419  grlicref  48504  gpgprismgr4cycllem10  48596  grlimedgnedg  48623  funcringcsetcALTV2lem6  48787  funcringcsetcALTV2lem7  48788  funcringcsetcALTV2lem9  48790  funcringcsetclem6ALTV  48810  funcringcsetclem7ALTV  48811  funcringcsetclem9ALTV  48813  dflinc2  48902  tposideq  49379  imaidfu  49601  opf2  49897  oduoppcciso  50057