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

Theorem fvi 5724
Description: The value of the identity function. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
fvi  |-  ( A  e.  V  ->  (  _I  `  A )  =  A )

Proof of Theorem fvi
StepHypRef Expression
1 funi 5425 . 2  |-  Fun  _I
2 ididg 4968 . 2  |-  ( A  e.  V  ->  A  _I  A )
3 funbrfv 5706 . 2  |-  ( Fun 
_I  ->  ( A  _I  A  ->  (  _I  `  A )  =  A ) )
41, 2, 3mpsyl 61 1  |-  ( A  e.  V  ->  (  _I  `  A )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   class class class wbr 4155    _I cid 4436   Fun wfun 5390   ` cfv 5396
This theorem is referenced by:  fviss  5725  fvmpti  5746  fvmpt2  5753  fvresi  5865  seqom0g  6651  fodomfi  7323  seqfeq4  11301  fac1  11499  facp1  11500  bcval5  11538  bcn2  11539  ids1  11680  s1val  11681  climshft2  12305  sum2id  12431  sumss  12447  strfvi  13436  xpsc0  13714  xpsc1  13715  grpinvfvi  14775  mulgfvi  14823  efgrcl  15276  efgval  15278  frgp0  15321  frgpmhm  15326  vrgpf  15329  vrgpinv  15330  frgpupf  15334  frgpup1  15336  frgpup2  15337  frgpup3lem  15338  frgpnabllem1  15413  frgpnabllem2  15414  rlmsca2  16201  ply1basfvi  16564  ply1plusgfvi  16565  psr1sca2  16574  ply1sca2  16577  ply1scl0  16610  ply1scl1  16612  indislem  16989  2ndcctbss  17441  1stcelcls  17447  txindislem  17588  iscau3  19104  iscmet3  19119  ovolctb  19255  itg2splitlem  19509  deg1fvi  19877  deg1invg  19898  dgrle  20031  logfac  20364  ginvsn  21787  ptpcon  24701  prod2id  25035  fprodfac  25077  dicvscacl  31308
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 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346
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 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-sbc 3107  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-iota 5360  df-fun 5398  df-fv 5404
  Copyright terms: Public domain W3C validator