Theorem fvi 6903

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   class class class wbr 5095   I cid 5517  Fun wfun 6480  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  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 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fviss  6904  fvmpti  6933  fvmpt2  6945  fvresi  7113  seqom0g  8385  fodomfi  9219  fodomfiOLD  9239  seqfeq4  13976  fac1  14202  facp1  14203  bcval5  14243  bcn2  14244  ids1  14522  s1val  14523  climshft2  15507  sum2id  15633  sumss  15649  prod2id  15853  fprodfac  15898  strfvi  17119  grpinvfvi  18879  mulgfvi  18970  efgrcl  19612  efgval  19614  frgp0  19657  frgpmhm  19662  vrgpf  19665  vrgpinv  19666  frgpupf  19670  frgpup1  19672  frgpup2  19673  frgpup3lem  19674  frgpnabllem1  19770  frgpnabllem2  19771  rlmsca2  21121  ply1basfvi  22141  ply1plusgfvi  22142  psr1sca2  22151  ply1sca2  22154  ply1scl0OLD  22193  ply1scl1OLD  22196  indislem  22903  2ndcctbss  23358  1stcelcls  23364  txindislem  23536  iscau3  25194  iscmet3  25209  ovolctb  25407  itg2splitlem  25665  deg1fvi  26006  deg1invg  26027  dgrle  26164  logfac  26526  fnpreimac  32628  ptpconn  35208  dicvscacl  41173  elinlem  43574  brfvid  43663  fvilbd  43665  nregmodelf1o  44992  cjnpoly  46877  tposid  48873  tposidres  48874