Theorem fvi 6906

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   class class class wbr 5095   I cid 5515  Fun wfun 6482  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6444  df-fun 6490  df-fv 6496

This theorem is referenced by:  fviss  6907  fvmpti  6936  fvmpt2  6948  fvresi  7115  seqom0g  8383  fodomfi  9205  fodomfiOLD  9223  seqfeq4  13962  fac1  14188  facp1  14189  bcval5  14229  bcn2  14230  ids1  14509  s1val  14510  climshft2  15493  sum2id  15619  sumss  15635  prod2id  15839  fprodfac  15884  strfvi  17105  grpinvfvi  18899  mulgfvi  18990  efgrcl  19631  efgval  19633  frgp0  19676  frgpmhm  19681  vrgpf  19684  vrgpinv  19685  frgpupf  19689  frgpup1  19691  frgpup2  19692  frgpup3lem  19693  frgpnabllem1  19789  frgpnabllem2  19790  rlmsca2  21137  ply1basfvi  22156  ply1plusgfvi  22157  psr1sca2  22166  ply1sca2  22169  ply1scl0OLD  22208  ply1scl1OLD  22211  indislem  22918  2ndcctbss  23373  1stcelcls  23379  txindislem  23551  iscau3  25208  iscmet3  25223  ovolctb  25421  itg2splitlem  25679  deg1fvi  26020  deg1invg  26041  dgrle  26178  logfac  26540  fnpreimac  32657  ptpconn  35300  dicvscacl  41313  elinlem  43718  brfvid  43807  fvilbd  43809  nregmodelf1o  45135  cjnpoly  47016  tposid  49012  tposidres  49013