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

Theorem fvi 5934
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 5627 . 2  |-  Fun  _I
2 ididg 5003 . 2  |-  ( A  e.  V  ->  A  _I  A )
3 funbrfv 5915 . 2  |-  ( Fun 
_I  ->  ( A  _I  A  ->  (  _I  `  A )  =  A ) )
41, 2, 3mpsyl 65 1  |-  ( A  e.  V  ->  (  _I  `  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1868   class class class wbr 4420    _I cid 4759   Fun wfun 5591   ` cfv 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pr 4656
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-iota 5561  df-fun 5599  df-fv 5605
This theorem is referenced by:  fviss  5935  fvmpti  5959  fvmpt2  5969  fvresi  6101  seqom0g  7177  fodomfi  7852  seqfeq4  12261  fac1  12462  facp1  12463  bcval5  12502  bcn2  12503  ids1  12726  s1val  12727  climshft2  13631  sum2id  13759  sumss  13775  prod2id  13967  fprodfac  14012  strfvi  15148  xpsc0  15451  xpsc1  15452  grpinvfvi  16692  mulgfvi  16747  efgrcl  17350  efgval  17352  frgp0  17395  frgpmhm  17400  vrgpf  17403  vrgpinv  17404  frgpupf  17408  frgpup1  17410  frgpup2  17411  frgpup3lem  17412  frgpnabllem1  17494  frgpnabllem2  17495  rlmsca2  18409  ply1basfvi  18819  ply1plusgfvi  18820  psr1sca2  18829  ply1sca2  18832  ply1scl0  18868  ply1scl1  18870  indislem  19999  2ndcctbss  20454  1stcelcls  20460  txindislem  20632  iscau3  22232  iscmet3  22247  ovolctb  22427  itg2splitlem  22690  deg1fvi  23018  deg1invg  23039  dgrle  23181  logfac  23534  ginvsn  26060  ptpcon  29949  dicvscacl  34675  brfvid  36136  fvilbd  36138
  Copyright terms: Public domain W3C validator