Theorem fvi 6910

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 6524	. 2 ⊢ Fun I
2		ididg 5802	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
3		funbrfv 6882	. 2 ⊢ (Fun I → (𝐴 I 𝐴 → ( I ‘𝐴) = 𝐴))
4	1, 2, 3	mpsyl 68	1 ⊢ (𝐴 ∈ 𝑉 → ( I ‘𝐴) = 𝐴)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   class class class wbr 5098   I cid 5518  Fun wfun 6486  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fviss  6911  fvmpti  6940  fvmpt2  6952  fvresi  7119  seqom0g  8387  fodomfi  9212  fodomfiOLD  9230  seqfeq4  13974  fac1  14200  facp1  14201  bcval5  14241  bcn2  14242  ids1  14521  s1val  14522  climshft2  15505  sum2id  15631  sumss  15647  prod2id  15851  fprodfac  15896  strfvi  17117  grpinvfvi  18912  mulgfvi  19003  efgrcl  19644  efgval  19646  frgp0  19689  frgpmhm  19694  vrgpf  19697  vrgpinv  19698  frgpupf  19702  frgpup1  19704  frgpup2  19705  frgpup3lem  19706  frgpnabllem1  19802  frgpnabllem2  19803  rlmsca2  21151  ply1basfvi  22181  ply1plusgfvi  22182  psr1sca2  22191  ply1sca2  22194  ply1scl0OLD  22233  ply1scl1OLD  22236  indislem  22944  2ndcctbss  23399  1stcelcls  23405  txindislem  23577  iscau3  25234  iscmet3  25249  ovolctb  25447  itg2splitlem  25705  deg1fvi  26046  deg1invg  26067  dgrle  26204  logfac  26566  fnpreimac  32749  ptpconn  35427  dicvscacl  41451  elinlem  43839  brfvid  43928  fvilbd  43930  nregmodelf1o  45256  cjnpoly  47135  tposid  49130  tposidres  49131