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

Theorem fvi 6722
Description: The value of the identity function. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
fvi (𝐴𝑉 → ( I ‘𝐴) = 𝐴)

Proof of Theorem fvi
StepHypRef Expression
1 funi 6366 . 2 Fun I
2 ididg 5701 . 2 (𝐴𝑉𝐴 I 𝐴)
3 funbrfv 6698 . 2 (Fun I → (𝐴 I 𝐴 → ( I ‘𝐴) = 𝐴))
41, 2, 3mpsyl 68 1 (𝐴𝑉 → ( I ‘𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2114   class class class wbr 5042   I cid 5436  Fun wfun 6328  cfv 6334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-id 5437  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-iota 6293  df-fun 6336  df-fv 6342
This theorem is referenced by:  fviss  6723  fvmpti  6749  fvmpt2  6761  fvresi  6917  seqom0g  8079  fodomfi  8785  seqfeq4  13415  fac1  13633  facp1  13634  bcval5  13674  bcn2  13675  ids1  13942  s1val  13943  climshft2  14930  sum2id  15056  sumss  15072  prod2id  15273  fprodfac  15318  strfvi  16528  grpinvfvi  18137  mulgfvi  18221  efgrcl  18832  efgval  18834  frgp0  18877  frgpmhm  18882  vrgpf  18885  vrgpinv  18886  frgpupf  18890  frgpup1  18892  frgpup2  18893  frgpup3lem  18894  frgpnabllem1  18984  frgpnabllem2  18985  rlmsca2  19964  ply1basfvi  20868  ply1plusgfvi  20869  psr1sca2  20878  ply1sca2  20881  ply1scl0  20917  ply1scl1  20919  indislem  21603  2ndcctbss  22058  1stcelcls  22064  txindislem  22236  iscau3  23880  iscmet3  23895  ovolctb  24092  itg2splitlem  24350  deg1fvi  24684  deg1invg  24705  dgrle  24838  logfac  25190  fnpreimac  30424  ptpconn  32554  dicvscacl  38445  elinlem  40228  brfvid  40318  fvilbd  40320
  Copyright terms: Public domain W3C validator