Theorem fvi 6954

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 6565	. 2 ⊢ Fun I
2		ididg 5833	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
3		funbrfv 6926	. 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 5549  Fun wfun 6527  ‘cfv 6533

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 2732  ax-sep 5251  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541

This theorem is used by:  fviss  6955  fvmpti  6985  fvmpt2  6998  fvresi  7171  seqom0g  8445  fodomfi  9282  seqfeq4  14115  fac1  14341  facp1  14342  bcval5  14382  bcn2  14383  ids1  14664  s1val  14665  climshft2  15669  sum2id  15794  sumss  15810  prod2id  16015  fprodfac  16060  strfvi  17282  grpinvfvi  19106  mulgfvi  19196  efgrcl  19842  efgval  19844  frgp0  19887  frgpmhm  19892  vrgpf  19895  vrgpinv  19896  frgpupf  19900  frgpup1  19902  frgpup2  19903  frgpup3lem  19904  frgpnabllem1  20000  frgpnabllem2  20001  rlmsca2  21383  ply1basfvi  22465  ply1plusgfvi  22466  psr1sca2  22475  ply1sca2  22478  indislem  23225  2ndcctbss  23681  1stcelcls  23687  txindislem  23859  iscau3  25506  iscmet3  25521  ovolctb  25718  itg2splitlem  25976  deg1fvi  26310  deg1invg  26331  dgrle  26469  logfac  26838  fnpreimac  33143  ptpconn  35812  dicvscacl  42064  elinlem  44438  brfvid  44527  fvilbd  44529  nregmodelf1o  45838  cjnpoly  47757  sqrtnpoly  47761  tposid  49811  tposidres  49812