Theorem fvi 6959

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 6570	. 2 ⊢ Fun I
2		ididg 5831	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
3		funbrfv 6931	. 2 ⊢ (Fun I → (𝐴 I 𝐴 → ( I ‘𝐴) = 𝐴))
4	1, 2, 3	mpsyl 69	1 ⊢ (𝐴 ∈ 𝑉 → ( I ‘𝐴) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   class class class wbr 5103   I cid 5545  Fun wfun 6531  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  fviss  6960  fvmpti  6990  fvmpt2  7003  fvresi  7176  seqom0g  8459  fodomfi  9297  seqfeq4  14187  fac1  14414  facp1  14415  bcval5  14455  bcn2  14456  ids1  14737  s1val  14738  climshft2  15742  sum2id  15867  sumss  15883  prod2id  16088  fprodfac  16133  strfvi  17361  grpinvfvi  19186  mulgfvi  19276  efgrcl  19922  efgval  19924  frgp0  19967  frgpmhm  19972  vrgpf  19975  vrgpinv  19976  frgpupf  19980  frgpup1  19982  frgpup2  19983  frgpup3lem  19984  frgpnabllem1  20080  frgpnabllem2  20081  rlmsca2  21467  ply1basfvi  22551  ply1plusgfvi  22552  psr1sca2  22561  ply1sca2  22564  indislem  23311  2ndcctbss  23767  1stcelcls  23773  txindislem  23945  iscau3  25592  iscmet3  25607  ovolctb  25804  itg2splitlem  26062  deg1fvi  26396  deg1invg  26417  dgrle  26555  logfac  26922  fnpreimac  33257  ptpconn  35977  dicvscacl  42228  elinlem  44583  brfvid  44672  fvilbd  44674  nregmodelf1o  45983  cjnpoly  47908  sqrtnpoly  47912  tposid  49962  tposidres  49963