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

Theorem fvi 5930
Description: The value of the identity function. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
fvi

Proof of Theorem fvi
StepHypRef Expression
1 funi 5623 . 2
2 ididg 5161 . 2
3 funbrfv 5911 . 2
41, 2, 3mpsyl 63 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818   class class class wbr 4452   cid 4795  Funwfun 5587  `cfv 5593
This theorem is referenced by:  fviss  5931  fvmpti  5955  fvmpt2  5963  fvresi  6097  seqom0g  7140  fodomfi  7819  seqfeq4  12156  fac1  12357  facp1  12358  bcval5  12396  bcn2  12397  ids1  12609  s1val  12610  climshft2  13405  sum2id  13530  sumss  13546  prod2id  13735  fprodfac  13777  strfvi  14672  xpsc0  14957  xpsc1  14958  grpinvfvi  16091  mulgfvi  16146  efgrcl  16733  efgval  16735  frgp0  16778  frgpmhm  16783  vrgpf  16786  vrgpinv  16787  frgpupf  16791  frgpup1  16793  frgpup2  16794  frgpup3lem  16795  frgpnabllem1  16877  frgpnabllem2  16878  rlmsca2  17847  ply1basfvi  18282  ply1plusgfvi  18283  psr1sca2  18292  ply1sca2  18295  ply1scl0  18331  ply1scl1  18333  indislem  19501  2ndcctbss  19956  1stcelcls  19962  txindislem  20134  iscau3  21717  iscmet3  21732  ovolctb  21901  itg2splitlem  22155  deg1fvi  22485  deg1invg  22507  dgrle  22640  logfac  22985  ginvsn  25351  ptpcon  28678  dicvscacl  36918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fv 5601
  Copyright terms: Public domain W3C validator