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 1542   ∈ wcel 2114   class class class wbr 5086   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 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 2709  ax-sep 5231  ax-pr 5370

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  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  6953  fvresi  7121  seqom0g  8388  fodomfi  9215  fodomfiOLD  9233  seqfeq4  14004  fac1  14230  facp1  14231  bcval5  14271  bcn2  14272  ids1  14551  s1val  14552  climshft2  15535  sum2id  15661  sumss  15677  prod2id  15884  fprodfac  15929  strfvi  17151  grpinvfvi  18949  mulgfvi  19040  efgrcl  19681  efgval  19683  frgp0  19726  frgpmhm  19731  vrgpf  19734  vrgpinv  19735  frgpupf  19739  frgpup1  19741  frgpup2  19742  frgpup3lem  19743  frgpnabllem1  19839  frgpnabllem2  19840  rlmsca2  21186  ply1basfvi  22214  ply1plusgfvi  22215  psr1sca2  22224  ply1sca2  22227  indislem  22975  2ndcctbss  23430  1stcelcls  23436  txindislem  23608  iscau3  25255  iscmet3  25270  ovolctb  25467  itg2splitlem  25725  deg1fvi  26060  deg1invg  26081  dgrle  26218  logfac  26578  fnpreimac  32758  ptpconn  35431  dicvscacl  41651  elinlem  44043  brfvid  44132  fvilbd  44134  nregmodelf1o  45460  cjnpoly  47349  tposid  49372  tposidres  49373