Theorem fvi 6715

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   class class class wbr 5030   I cid 5424  Fun wfun 6318  ‘cfv 6324

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-iota 6283  df-fun 6326  df-fv 6332

This theorem is referenced by:  fviss  6716  fvmpti  6744  fvmpt2  6756  fvresi  6912  seqom0g  8075  fodomfi  8781  seqfeq4  13415  fac1  13633  facp1  13634  bcval5  13674  bcn2  13675  ids1  13942  s1val  13943  climshft2  14931  sum2id  15057  sumss  15073  prod2id  15274  fprodfac  15319  strfvi  16529  grpinvfvi  18138  mulgfvi  18222  efgrcl  18833  efgval  18835  frgp0  18878  frgpmhm  18883  vrgpf  18886  vrgpinv  18887  frgpupf  18891  frgpup1  18893  frgpup2  18894  frgpup3lem  18895  frgpnabllem1  18986  frgpnabllem2  18987  rlmsca2  19966  ply1basfvi  20870  ply1plusgfvi  20871  psr1sca2  20880  ply1sca2  20883  ply1scl0  20919  ply1scl1  20921  indislem  21605  2ndcctbss  22060  1stcelcls  22066  txindislem  22238  iscau3  23882  iscmet3  23897  ovolctb  24094  itg2splitlem  24352  deg1fvi  24686  deg1invg  24707  dgrle  24840  logfac  25192  fnpreimac  30434  ptpconn  32593  dicvscacl  38487  elinlem  40298  brfvid  40388  fvilbd  40390