Theorem fvi 6955

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

Step	Hyp	Ref	Expression
1		funi 6566	. 2 ⊢ Fun I
2		ididg 5837	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
3		funbrfv 6927	. 2 ⊢ (Fun I → (𝐴 I 𝐴 → ( I ‘𝐴) = 𝐴))
4	1, 2, 3	mpsyl 69	1 ⊢ (𝐴 ∈ 𝑉 → ( I ‘𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   class class class wbr 5110   I cid 5553  Fun wfun 6528  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6490  df-fun 6536  df-fv 6542

This theorem is referenced by:  fviss  6956  fvmpti  6986  fvmpt2  6999  fvresi  7169  seqom0g  8439  fodomfi  9268  seqfeq4  14083  fac1  14309  facp1  14310  bcval5  14350  bcn2  14351  ids1  14631  s1val  14632  climshft2  15629  sum2id  15755  sumss  15771  prod2id  15978  fprodfac  16023  strfvi  17246  grpinvfvi  19045  mulgfvi  19135  efgrcl  19781  efgval  19783  frgp0  19826  frgpmhm  19831  vrgpf  19834  vrgpinv  19835  frgpupf  19839  frgpup1  19841  frgpup2  19842  frgpup3lem  19843  frgpnabllem1  19939  frgpnabllem2  19940  rlmsca2  21294  ply1basfvi  22365  ply1plusgfvi  22366  psr1sca2  22375  ply1sca2  22378  indislem  23122  2ndcctbss  23577  1stcelcls  23583  txindislem  23755  iscau3  25402  iscmet3  25417  ovolctb  25614  itg2splitlem  25872  deg1fvi  26207  deg1invg  26228  dgrle  26365  logfac  26728  fnpreimac  32952  ptpconn  35620  dicvscacl  41850  elinlem  44211  brfvid  44300  fvilbd  44302  nregmodelf1o  45611  cjnpoly  47510  tposid  49543  tposidres  49544