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

Theorem fvi 5775
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 5475 . 2  |-  Fun  _I
2 ididg 5018 . 2  |-  ( A  e.  V  ->  A  _I  A )
3 funbrfv 5757 . 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 1652    e. wcel 1725   class class class wbr 4204    _I cid 4485   Fun wfun 5440   ` cfv 5446
This theorem is referenced by:  fviss  5776  fvmpti  5797  fvmpt2  5804  fvresi  5916  seqom0g  6705  fodomfi  7377  seqfeq4  11364  fac1  11562  facp1  11563  bcval5  11601  bcn2  11602  ids1  11743  s1val  11744  climshft2  12368  sum2id  12494  sumss  12510  strfvi  13499  xpsc0  13777  xpsc1  13778  grpinvfvi  14838  mulgfvi  14886  efgrcl  15339  efgval  15341  frgp0  15384  frgpmhm  15389  vrgpf  15392  vrgpinv  15393  frgpupf  15397  frgpup1  15399  frgpup2  15400  frgpup3lem  15401  frgpnabllem1  15476  frgpnabllem2  15477  rlmsca2  16264  ply1basfvi  16627  ply1plusgfvi  16628  psr1sca2  16637  ply1sca2  16640  ply1scl0  16673  ply1scl1  16675  indislem  17056  2ndcctbss  17510  1stcelcls  17516  txindislem  17657  iscau3  19223  iscmet3  19238  ovolctb  19378  itg2splitlem  19632  deg1fvi  20000  deg1invg  20021  dgrle  20154  logfac  20487  ginvsn  21929  ptpcon  24912  prod2id  25246  fprodfac  25288  dicvscacl  31916
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-iota 5410  df-fun 5448  df-fv 5454
  Copyright terms: Public domain W3C validator