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

Theorem fvresi 6016
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 5816 . 2  |-  ( B  e.  A  ->  (
(  _I  |`  A ) `
 B )  =  (  _I  `  B
) )
2 fvi 5860 . 2  |-  ( B  e.  A  ->  (  _I  `  B )  =  B )
31, 2eqtrd 2495 1  |-  ( B  e.  A  ->  (
(  _I  |`  A ) `
 B )  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758    _I cid 4742    |` cres 4953   ` cfv 5529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-sbc 3295  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-uni 4203  df-br 4404  df-opab 4462  df-id 4747  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-res 4963  df-iota 5492  df-fun 5531  df-fv 5537
This theorem is referenced by:  fninfp  6017  fndifnfp  6019  fnnfpeq0  6021  f1ocnvfv1  6095  f1ocnvfv2  6096  fcof1  6103  fcofo  6104  isoid  6132  weniso  6157  iordsmo  6931  fipreima  7731  infxpenc  8299  infxpencOLD  8304  dfac9  8420  ndxarg  14316  idfu2  14911  idfu1  14913  idfucl  14914  cofurid  14924  yonedainv  15214  idghm  15885  lactghmga  16032  symgga  16034  cayleylem2  16041  gsmsymgrfix  16056  gsmsymgreq  16060  pmtrfinv  16090  idlmhm  17255  evl1vard  17906  islinds2  18377  lindsind2  18383  madetsumid  18483  mdetunilem7  18566  txkgen  19367  ustuqtop3  19960  iducn  20000  nmoid  20463  dvid  21535  mvth  21607  fta1blem  21783  qaa  21932  dfiop2  25336  idunop  25561  idcnop  25564  elunop2  25596  lnophm  25602  qqhre  26614  subfacp1lem4  27238  subfacp1lem5  27239  cvmliftlem5  27345  ghomsn  27474  rngunsnply  29701  dflinc2  31099  idlaut  34103  idldil  34121  ltrnid  34142  idltrn  34157  ltrnideq  34182  tendoidcl  34776  tendo1ne0  34835  cdleml7  34989  tendospid  35025  dvalveclem  35033
  Copyright terms: Public domain W3C validator