Theorem fvresi 7188

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146   I cid 5549   ↾ cres 5657  ‘cfv 6547

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-res 5667  df-iota 6501  df-fun 6549  df-fv 6555

This theorem is used by:  fninfp  7189  fndifnfp  7191  fnnfpeq0  7193  f1ocnvfv1  7294  f1ocnvfv2  7295  fcof1  7305  fcofo  7306  isoid  7347  weniso  7374  iordsmo  8379  fipreima  9361  infxpenc  10110  dfac9  10228  fproddvdsd  16520  ndxarg  17389  idfu2  18068  idfu1  18070  idfucl  18071  cofurid  18081  funcestrcsetclem6  18334  funcestrcsetclem7  18335  funcestrcsetclem9  18337  funcsetcestrclem6  18349  funcsetcestrclem7  18350  funcsetcestrclem9  18352  yonedainv  18470  idmgmhm  18905  idmhm  19005  smndex1n0mnd  19126  idghm  19460  lactghmga  19634  symgga  19636  cayleylem2  19642  gsmsymgrfix  19657  gsmsymgreq  19661  pmtrfinv  19690  funcrngcsetcALT  20908  idlmhm  21331  islinds2  22134  lindsind2  22140  psdmplcl  22498  evl1vard  22670  evls1varpwval  22701  madetsumid  22791  mdetunilem7  22948  txkgen  23986  ustuqtop3  24577  iducn  24616  nmoid  25076  dvid  26253  mvth  26327  fta1blem  26504  idpfv  26543  idmot  29015  dfiop2  32370  idunop  32595  idcnop  32598  elunop2  32630  lnophm  32636  fcobijfs2  33370  fzo0pmtrlast  33709  pmtridfv1  33712  pmtridfv2  33713  cycpmfv3  33732  islinds5  33979  ellspds  33980  vr1nz  34181  algextdeglem4  34408  2sqr3minply  34468  cos9thpiminplylem6  34475  qqhre  34708  subfacp1lem4  36072  subfacp1lem5  36073  cvmliftlem5  36178  bj-evalid  38139  idlaut  41296  idldil  41314  ltrnid  41335  idltrn  41350  ltrnideq  41375  tendoidcl  41969  tendo1ne0  42028  cdleml7  42182  dvalveclem  42225  dvhlveclem  42308  cdlemn8  42404  cdlemn11a  42407  rngunsnply  44314  fundcmpsurbijinjpreimafv  48631  fundcmpsurinjimaid  48635  grimidvtxedg  49125  gricushgr  49157  ushggricedg  49167  grlicref  49252  gpgprismgr4cycllem10  49344  grlimedgnedg  49371  funcringcsetcALTV2lem6  49534  funcringcsetcALTV2lem7  49535  funcringcsetcALTV2lem9  49537  funcringcsetclem6ALTV  49557  funcringcsetclem7ALTV  49558  funcringcsetclem9ALTV  49560  dflinc2  49664  tposideq  50143  imaidfu  50368  opf2  50683  termccofix  50813  oduoppcciso  50846  parmapfunc2  50916  parmapfunc  50917