Theorem fvi 6853

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107   class class class wbr 5075   I cid 5489  Fun wfun 6431  ‘cfv 6437

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

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 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445

This theorem is referenced by:  fviss  6854  fvmpti  6883  fvmpt2  6895  fvresi  7054  seqom0g  8296  fodomfi  9101  seqfeq4  13781  fac1  14000  facp1  14001  bcval5  14041  bcn2  14042  ids1  14311  s1val  14312  climshft2  15300  sum2id  15429  sumss  15445  prod2id  15647  fprodfac  15692  strfvi  16900  grpinvfvi  18631  mulgfvi  18715  efgrcl  19330  efgval  19332  frgp0  19375  frgpmhm  19380  vrgpf  19383  vrgpinv  19384  frgpupf  19388  frgpup1  19390  frgpup2  19391  frgpup3lem  19392  frgpnabllem1  19483  frgpnabllem2  19484  rlmsca2  20480  ply1basfvi  21421  ply1plusgfvi  21422  psr1sca2  21431  ply1sca2  21434  ply1scl0  21470  ply1scl1  21472  indislem  22159  2ndcctbss  22615  1stcelcls  22621  txindislem  22793  iscau3  24451  iscmet3  24466  ovolctb  24663  itg2splitlem  24922  deg1fvi  25259  deg1invg  25280  dgrle  25413  logfac  25765  fnpreimac  31017  ptpconn  33204  dicvscacl  39212  elinlem  41213  brfvid  41302  fvilbd  41304