Theorem fvi 6916

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   class class class wbr 5085   I cid 5525  Fun wfun 6492  ‘cfv 6498

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506

This theorem is referenced by:  fviss  6917  fvmpti  6946  fvmpt2  6959  fvresi  7128  seqom0g  8395  fodomfi  9222  fodomfiOLD  9240  seqfeq4  14013  fac1  14239  facp1  14240  bcval5  14280  bcn2  14281  ids1  14560  s1val  14561  climshft2  15544  sum2id  15670  sumss  15686  prod2id  15893  fprodfac  15938  strfvi  17160  grpinvfvi  18958  mulgfvi  19049  efgrcl  19690  efgval  19692  frgp0  19735  frgpmhm  19740  vrgpf  19743  vrgpinv  19744  frgpupf  19748  frgpup1  19750  frgpup2  19751  frgpup3lem  19752  frgpnabllem1  19848  frgpnabllem2  19849  rlmsca2  21194  ply1basfvi  22204  ply1plusgfvi  22205  psr1sca2  22214  ply1sca2  22217  indislem  22965  2ndcctbss  23420  1stcelcls  23426  txindislem  23598  iscau3  25245  iscmet3  25260  ovolctb  25457  itg2splitlem  25715  deg1fvi  26050  deg1invg  26071  dgrle  26208  logfac  26565  fnpreimac  32743  ptpconn  35415  dicvscacl  41637  elinlem  44025  brfvid  44114  fvilbd  44116  nregmodelf1o  45442  cjnpoly  47337  tposid  49360  tposidres  49361