Theorem fvresi 7129

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   I cid 5525   ↾ cres 5633  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-res 5643  df-iota 6452  df-fun 6501  df-fv 6507

This theorem is referenced by:  fninfp  7130  fndifnfp  7132  fnnfpeq0  7134  f1ocnvfv1  7233  f1ocnvfv2  7234  fcof1  7244  fcofo  7245  isoid  7286  weniso  7311  iordsmo  8303  fipreima  9285  infxpenc  9947  dfac9  10066  fproddvdsd  16281  ndxarg  17142  idfu2  17820  idfu1  17822  idfucl  17823  cofurid  17833  funcestrcsetclem6  18086  funcestrcsetclem7  18087  funcestrcsetclem9  18089  funcsetcestrclem6  18101  funcsetcestrclem7  18102  funcsetcestrclem9  18104  yonedainv  18222  idmgmhm  18610  idmhm  18704  smndex1n0mnd  18821  idghm  19145  lactghmga  19319  symgga  19321  cayleylem2  19327  gsmsymgrfix  19342  gsmsymgreq  19346  pmtrfinv  19375  funcrngcsetcALT  20561  idlmhm  20980  islinds2  21755  lindsind2  21761  psdmplcl  22082  evl1vard  22257  evls1varpwval  22288  madetsumid  22381  mdetunilem7  22538  txkgen  23572  ustuqtop3  24164  iducn  24203  nmoid  24663  dvid  25852  mvth  25930  fta1blem  26109  qaa  26264  idmot  28517  dfiop2  31732  idunop  31957  idcnop  31960  elunop2  31992  lnophm  31998  fzo0pmtrlast  33064  pmtridfv1  33067  pmtridfv2  33068  cycpmfv3  33087  islinds5  33331  ellspds  33332  vr1nz  33552  algextdeglem4  33703  2sqr3minply  33763  cos9thpiminplylem6  33770  qqhre  34003  subfacp1lem4  35163  subfacp1lem5  35164  cvmliftlem5  35269  bj-evalid  37057  idlaut  40083  idldil  40101  ltrnid  40122  idltrn  40137  ltrnideq  40162  tendoidcl  40756  tendo1ne0  40815  cdleml7  40969  dvalveclem  41012  dvhlveclem  41095  cdlemn8  41191  cdlemn11a  41194  rngunsnply  43151  fundcmpsurbijinjpreimafv  47401  fundcmpsurinjimaid  47405  grimidvtxedg  47878  gricushgr  47910  ushggricedg  47920  grlicref  47997  gpgprismgr4cycllem10  48087  funcringcsetcALTV2lem6  48276  funcringcsetcALTV2lem7  48277  funcringcsetcALTV2lem9  48279  funcringcsetclem6ALTV  48299  funcringcsetclem7ALTV  48300  funcringcsetclem9ALTV  48302  dflinc2  48392  tposideq  48869  imaidfu  49092  opf2  49388  oduoppcciso  49548