MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvresi Unicode version

Theorem fvresi 5883
Description: The value of a restricted identity function. (Contributed by NM, 19-May-2004.)
Assertion
Ref Expression
fvresi  |-  ( B  e.  A  ->  (
(  _I  |`  A ) `
 B )  =  B )

Proof of Theorem fvresi
StepHypRef Expression
1 fvres 5704 . 2  |-  ( B  e.  A  ->  (
(  _I  |`  A ) `
 B )  =  (  _I  `  B
) )
2 fvi 5742 . 2  |-  ( B  e.  A  ->  (  _I  `  B )  =  B )
31, 2eqtrd 2436 1  |-  ( B  e.  A  ->  (
(  _I  |`  A ) `
 B )  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721    _I cid 4453    |` cres 4839   ` cfv 5413
This theorem is referenced by:  f1ocnvfv1  5973  f1ocnvfv2  5974  fcof1  5979  fcofo  5980  isoid  6008  weniso  6034  iordsmo  6578  fipreima  7370  infxpenc  7855  dfac9  7972  ndxarg  13444  idfu2  14030  idfu1  14032  idfucl  14033  cofurid  14043  yonedainv  14333  idghm  14976  lactghmga  15062  symgga  15064  cayleylem2  15066  idlmhm  16072  txkgen  17637  ustuqtop3  18226  iducn  18266  nmoid  18729  dvid  19757  mvth  19829  evl1vard  19906  fta1blem  20044  qaa  20193  dfiop2  23209  idunop  23434  idcnop  23437  elunop2  23469  lnophm  23475  qqhre  24339  subfacp1lem4  24822  subfacp1lem5  24823  cvmliftlem5  24929  ghomsn  25052  fninfp  26625  fndifnfp  26627  fnnfpeq0  26629  islinds2  27151  lindsind2  27157  rngunsnply  27246  pmtrfinv  27270  idlaut  30578  idldil  30596  ltrnid  30617  idltrn  30632  ltrnideq  30657  tendoidcl  31251  tendo1ne0  31310  cdleml7  31464  tendospid  31500  dvalveclem  31508
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-res 4849  df-iota 5377  df-fun 5415  df-fv 5421
  Copyright terms: Public domain W3C validator