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

Theorem fvi 5747
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 5447 . 2  |-  Fun  _I
2 ididg 4992 . 2  |-  ( A  e.  V  ->  A  _I  A )
3 funbrfv 5729 . 2  |-  ( Fun 
_I  ->  ( A  _I  A  ->  (  _I  `  A )  =  A ) )
41, 2, 3mpsyl 63 1  |-  ( A  e.  V  ->  (  _I  `  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   class class class wbr 4291    _I cid 4630   Fun wfun 5411   ` cfv 5417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pr 4530
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-sbc 3186  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-opab 4350  df-id 4635  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-iota 5380  df-fun 5419  df-fv 5425
This theorem is referenced by:  fviss  5748  fvmpti  5772  fvmpt2  5780  fvresi  5903  seqom0g  6910  fodomfi  7589  seqfeq4  11854  fac1  12054  facp1  12055  bcval5  12093  bcn2  12094  ids1  12288  s1val  12289  climshft2  13059  sum2id  13184  sumss  13200  strfvi  14213  xpsc0  14497  xpsc1  14498  grpinvfvi  15578  mulgfvi  15630  efgrcl  16211  efgval  16213  frgp0  16256  frgpmhm  16261  vrgpf  16264  vrgpinv  16265  frgpupf  16269  frgpup1  16271  frgpup2  16272  frgpup3lem  16273  frgpnabllem1  16350  frgpnabllem2  16351  rlmsca2  17281  ply1basfvi  17695  ply1plusgfvi  17696  psr1sca2  17705  ply1sca2  17708  ply1scl0  17741  ply1scl1  17743  indislem  18603  2ndcctbss  19058  1stcelcls  19064  txindislem  19205  iscau3  20788  iscmet3  20803  ovolctb  20972  itg2splitlem  21225  deg1fvi  21555  deg1invg  21577  dgrle  21710  logfac  22048  ginvsn  23835  ptpcon  27121  prod2id  27440  fprodfac  27482  dicvscacl  34834
  Copyright terms: Public domain W3C validator