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

Theorem fvi 6417
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 6081 . 2 Fun I
2 ididg 5431 . 2 (𝐴𝑉𝐴 I 𝐴)
3 funbrfv 6395 . 2 (Fun I → (𝐴 I 𝐴 → ( I ‘𝐴) = 𝐴))
41, 2, 3mpsyl 68 1 (𝐴𝑉 → ( I ‘𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2139   class class class wbr 4804   I cid 5173  Fun wfun 6043  cfv 6049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-iota 6012  df-fun 6051  df-fv 6057
This theorem is referenced by:  fviss  6418  fvmpti  6443  fvmpt2  6453  fvresi  6603  seqom0g  7720  fodomfi  8404  seqfeq4  13044  fac1  13258  facp1  13259  bcval5  13299  bcn2  13300  ids1  13567  s1val  13568  climshft2  14512  sum2id  14638  sumss  14654  prod2id  14857  fprodfac  14902  strfvi  16115  xpsc0  16422  xpsc1  16423  grpinvfvi  17664  mulgfvi  17746  efgrcl  18328  efgval  18330  frgp0  18373  frgpmhm  18378  vrgpf  18381  vrgpinv  18382  frgpupf  18386  frgpup1  18388  frgpup2  18389  frgpup3lem  18390  frgpnabllem1  18476  frgpnabllem2  18477  rlmsca2  19403  ply1basfvi  19813  ply1plusgfvi  19814  psr1sca2  19823  ply1sca2  19826  ply1scl0  19862  ply1scl1  19864  indislem  21006  2ndcctbss  21460  1stcelcls  21466  txindislem  21638  iscau3  23276  iscmet3  23291  ovolctb  23458  itg2splitlem  23714  deg1fvi  24044  deg1invg  24065  dgrle  24198  logfac  24546  ptpconn  31522  dicvscacl  36982  elinlem  38406  brfvid  38481  fvilbd  38483
  Copyright terms: Public domain W3C validator