Theorem fvi 6838

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   class class class wbr 5075   I cid 5485  Fun wfun 6422  ‘cfv 6428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-id 5486  df-xp 5592  df-rel 5593  df-cnv 5594  df-co 5595  df-dm 5596  df-iota 6386  df-fun 6430  df-fv 6436

This theorem is referenced by:  fviss  6839  fvmpti  6868  fvmpt2  6880  fvresi  7039  seqom0g  8276  fodomfi  9081  seqfeq4  13761  fac1  13980  facp1  13981  bcval5  14021  bcn2  14022  ids1  14291  s1val  14292  climshft2  15280  sum2id  15409  sumss  15425  prod2id  15627  fprodfac  15672  strfvi  16880  grpinvfvi  18611  mulgfvi  18695  efgrcl  19310  efgval  19312  frgp0  19355  frgpmhm  19360  vrgpf  19363  vrgpinv  19364  frgpupf  19368  frgpup1  19370  frgpup2  19371  frgpup3lem  19372  frgpnabllem1  19463  frgpnabllem2  19464  rlmsca2  20460  ply1basfvi  21401  ply1plusgfvi  21402  psr1sca2  21411  ply1sca2  21414  ply1scl0  21450  ply1scl1  21452  indislem  22139  2ndcctbss  22595  1stcelcls  22601  txindislem  22773  iscau3  24431  iscmet3  24446  ovolctb  24643  itg2splitlem  24902  deg1fvi  25239  deg1invg  25260  dgrle  25393  logfac  25745  fnpreimac  30995  ptpconn  33182  dicvscacl  39192  elinlem  41166  brfvid  41255  fvilbd  41257