Theorem fvresi 7178

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   I cid 5545   ↾ cres 5653  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-res 5663  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is used by:  fninfp  7179  fndifnfp  7181  fnnfpeq0  7183  f1ocnvfv1  7284  f1ocnvfv2  7285  fcof1  7295  fcofo  7296  isoid  7337  weniso  7364  iordsmo  8365  fipreima  9347  infxpenc  10097  dfac9  10215  fproddvdsd  16505  ndxarg  17374  idfu2  18053  idfu1  18055  idfucl  18056  cofurid  18066  funcestrcsetclem6  18319  funcestrcsetclem7  18320  funcestrcsetclem9  18322  funcsetcestrclem6  18334  funcsetcestrclem7  18335  funcsetcestrclem9  18337  yonedainv  18455  idmgmhm  18890  idmhm  18990  smndex1n0mnd  19111  idghm  19445  lactghmga  19619  symgga  19621  cayleylem2  19627  gsmsymgrfix  19642  gsmsymgreq  19646  pmtrfinv  19675  funcrngcsetcALT  20893  idlmhm  21316  islinds2  22119  lindsind2  22125  psdmplcl  22483  evl1vard  22655  evls1varpwval  22686  madetsumid  22776  mdetunilem7  22933  txkgen  23971  ustuqtop3  24562  iducn  24601  nmoid  25061  dvid  26238  mvth  26312  fta1blem  26489  idpfv  26528  qaa  26647  idmot  29000  dfiop2  32355  idunop  32580  idcnop  32583  elunop2  32615  lnophm  32621  fcobijfs2  33314  fzo0pmtrlast  33653  pmtridfv1  33656  pmtridfv2  33657  cycpmfv3  33676  islinds5  33923  ellspds  33924  vr1nz  34125  algextdeglem4  34352  2sqr3minply  34412  cos9thpiminplylem6  34419  qqhre  34652  subfacp1lem4  35948  subfacp1lem5  35949  cvmliftlem5  36054  bj-evalid  37997  idlaut  41153  idldil  41171  ltrnid  41192  idltrn  41207  ltrnideq  41232  tendoidcl  41826  tendo1ne0  41885  cdleml7  42039  dvalveclem  42082  dvhlveclem  42165  cdlemn8  42261  cdlemn11a  42264  rngunsnply  44170  fundcmpsurbijinjpreimafv  48488  fundcmpsurinjimaid  48492  grimidvtxedg  48982  gricushgr  49014  ushggricedg  49024  grlicref  49109  gpgprismgr4cycllem10  49201  grlimedgnedg  49228  funcringcsetcALTV2lem6  49391  funcringcsetcALTV2lem7  49392  funcringcsetcALTV2lem9  49394  funcringcsetclem6ALTV  49414  funcringcsetclem7ALTV  49415  funcringcsetclem9ALTV  49417  dflinc2  49521  tposideq  49995  imaidfu  50217  opf2  50513  oduoppcciso  50673