Theorem fvi 6992

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   class class class wbr 5108   I cid 5552  Fun wfun 6560  ‘cfv 6566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5255  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fv 6574

This theorem is used by:  fviss  6993  fvmpti  7023  fvmpt2  7036  fvresi  7209  seqom0g  8504  fodomfi  9342  seqfeq4  14234  fac1  14462  facp1  14463  bcval5  14503  bcn2  14504  ids1  14785  s1val  14786  climshft2  15793  sum2id  15918  sumss  15934  prod2id  16139  fprodfac  16184  strfvi  17412  grpinvfvi  19243  mulgfvi  19333  efgrcl  19980  efgval  19982  frgp0  20025  frgpmhm  20030  vrgpf  20033  vrgpinv  20034  frgpupf  20038  frgpup1  20040  frgpup2  20041  frgpup3lem  20042  frgpnabllem1  20138  frgpnabllem2  20139  rlmsca2  21525  ply1basfvi  22613  ply1plusgfvi  22614  psr1sca2  22623  ply1sca2  22626  indislem  23373  2ndcctbss  23829  1stcelcls  23835  txindislem  24007  iscau3  25654  iscmet3  25669  ovolctb  25866  itg2splitlem  26124  deg1fvi  26458  deg1invg  26479  dgrle  26617  logfac  26986  fnpreimac  33362  ptpconn  36206  dicvscacl  42514  elinlem  44859  brfvid  44948  fvilbd  44950  nregmodelf1o  46269  cjnpoly  48212  sqrtnpoly  48216  tposid  50329  tposidres  50330