Theorem fvresi 6480

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

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030   I cid 5052   ↾ cres 5145  ‘cfv 5926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-res 5155  df-iota 5889  df-fun 5928  df-fv 5934

This theorem is referenced by:  fninfp  6481  fndifnfp  6483  fnnfpeq0  6485  f1ocnvfv1  6572  f1ocnvfv2  6573  fcof1  6582  fcofo  6583  isoid  6619  weniso  6644  iordsmo  7499  fipreima  8313  infxpenc  8879  dfac9  8996  fproddvdsd  15106  ndxarg  15929  idfu2  16585  idfu1  16587  idfucl  16588  cofurid  16598  funcestrcsetclem6  16832  funcestrcsetclem7  16833  funcestrcsetclem9  16835  funcsetcestrclem6  16847  funcsetcestrclem7  16848  funcsetcestrclem9  16850  yonedainv  16968  idmhm  17391  idghm  17722  lactghmga  17870  symgga  17872  cayleylem2  17879  gsmsymgrfix  17894  gsmsymgreq  17898  pmtrfinv  17927  idlmhm  19089  evl1vard  19749  islinds2  20200  lindsind2  20206  madetsumid  20315  mdetunilem7  20472  txkgen  21503  ustuqtop3  22094  iducn  22134  nmoid  22593  dvid  23726  mvth  23800  fta1blem  23973  qaa  24123  idmot  25477  dfiop2  28740  idunop  28965  idcnop  28968  elunop2  29000  lnophm  29006  pmtridfv1  29985  pmtridfv2  29986  qqhre  30192  subfacp1lem4  31291  subfacp1lem5  31292  cvmliftlem5  31397  bj-evalid  33153  idlaut  35700  idldil  35718  ltrnid  35739  idltrn  35754  ltrnideq  35780  tendoidcl  36374  tendo1ne0  36433  cdleml7  36587  tendospid  36623  dvalveclem  36631  rngunsnply  38060  idmgmhm  42113  funcrngcsetcALT  42324  funcringcsetcALTV2lem6  42366  funcringcsetcALTV2lem7  42367  funcringcsetcALTV2lem9  42369  funcringcsetclem6ALTV  42389  funcringcsetclem7ALTV  42390  funcringcsetclem9ALTV  42392  dflinc2  42524