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

Theorem fvresi 6073
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 5862 . 2  |-  ( B  e.  A  ->  (
(  _I  |`  A ) `
 B )  =  (  _I  `  B
) )
2 fvi 5905 . 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 1398    e. wcel 1823    _I cid 4779    |` cres 4990   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-res 5000  df-iota 5534  df-fun 5572  df-fv 5578
This theorem is referenced by:  fninfp  6074  fndifnfp  6076  fnnfpeq0  6078  f1ocnvfv1  6157  f1ocnvfv2  6158  fcof1  6165  fcofo  6166  isoid  6200  weniso  6225  iordsmo  7020  fipreima  7818  infxpenc  8386  infxpencOLD  8391  dfac9  8507  ndxarg  14736  idfu2  15366  idfu1  15368  idfucl  15369  cofurid  15379  funcestrcsetclem6  15613  funcestrcsetclem7  15614  funcestrcsetclem9  15616  funcsetcestrclem6  15628  funcsetcestrclem7  15629  funcsetcestrclem9  15631  yonedainv  15749  idmhm  16174  idghm  16481  lactghmga  16628  symgga  16630  cayleylem2  16637  gsmsymgrfix  16652  gsmsymgreq  16656  pmtrfinv  16685  idlmhm  17882  evl1vard  18568  islinds2  19015  lindsind2  19021  madetsumid  19130  mdetunilem7  19287  txkgen  20319  ustuqtop3  20912  iducn  20952  nmoid  21415  dvid  22487  mvth  22559  fta1blem  22735  qaa  22885  idmot  24125  dfiop2  26870  idunop  27095  idcnop  27098  elunop2  27130  lnophm  27136  qqhre  28232  subfacp1lem4  28891  subfacp1lem5  28892  cvmliftlem5  28998  ghomsn  29292  rngunsnply  31363  idmgmhm  32848  funcrngcsetcALT  33061  funcringcsetcALTV2lem6  33103  funcringcsetcALTV2lem7  33104  funcringcsetcALTV2lem9  33106  funcringcsetclem6ALTV  33126  funcringcsetclem7ALTV  33127  funcringcsetclem9ALTV  33129  dflinc2  33265  idlaut  36217  idldil  36235  ltrnid  36256  idltrn  36271  ltrnideq  36297  tendoidcl  36892  tendo1ne0  36951  cdleml7  37105  tendospid  37141  dvalveclem  37149
  Copyright terms: Public domain W3C validator