Theorem fvresi 6935

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   I cid 5459   ↾ cres 5557  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-res 5567  df-iota 6314  df-fun 6357  df-fv 6363

This theorem is referenced by:  fninfp  6936  fndifnfp  6938  fnnfpeq0  6940  f1ocnvfv1  7033  f1ocnvfv2  7034  fcof1  7043  fcofo  7044  isoid  7082  weniso  7107  iordsmo  7994  fipreima  8830  infxpenc  9444  dfac9  9562  fproddvdsd  15684  ndxarg  16508  idfu2  17148  idfu1  17150  idfucl  17151  cofurid  17161  funcestrcsetclem6  17395  funcestrcsetclem7  17396  funcestrcsetclem9  17398  funcsetcestrclem6  17410  funcsetcestrclem7  17411  funcsetcestrclem9  17413  yonedainv  17531  idmhm  17965  smndex1n0mnd  18077  idghm  18373  lactghmga  18533  symgga  18535  cayleylem2  18541  gsmsymgrfix  18556  gsmsymgreq  18560  pmtrfinv  18589  idlmhm  19813  evl1vard  20500  islinds2  20957  lindsind2  20963  madetsumid  21070  mdetunilem7  21227  txkgen  22260  ustuqtop3  22852  iducn  22892  nmoid  23351  dvid  24515  mvth  24589  fta1blem  24762  qaa  24912  idmot  26323  dfiop2  29530  idunop  29755  idcnop  29758  elunop2  29790  lnophm  29796  pmtridfv1  30737  pmtridfv2  30738  cycpmfv3  30757  islinds5  30932  ellspds  30933  qqhre  31261  subfacp1lem4  32430  subfacp1lem5  32431  cvmliftlem5  32536  bj-evalid  34370  idlaut  37247  idldil  37265  ltrnid  37286  idltrn  37301  ltrnideq  37326  tendoidcl  37920  tendo1ne0  37979  cdleml7  38133  dvalveclem  38176  dvhlveclem  38259  cdlemn8  38355  cdlemn11a  38358  rngunsnply  39793  fundcmpsurbijinjpreimafv  43587  fundcmpsurinjimaid  43591  isomgreqve  44010  isomushgr  44011  ushrisomgr  44026  idmgmhm  44075  funcrngcsetcALT  44290  funcringcsetcALTV2lem6  44332  funcringcsetcALTV2lem7  44333  funcringcsetcALTV2lem9  44335  funcringcsetclem6ALTV  44355  funcringcsetclem7ALTV  44356  funcringcsetclem9ALTV  44358  dflinc2  44485