Theorem fvi 6294

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

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030   class class class wbr 4685   I cid 5052  Fun wfun 5920  ‘cfv 5926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934

This theorem is referenced by:  fviss  6295  fvmpti  6320  fvmpt2  6330  fvresi  6480  seqom0g  7596  fodomfi  8280  seqfeq4  12890  fac1  13104  facp1  13105  bcval5  13145  bcn2  13146  ids1  13413  s1val  13414  climshft2  14357  sum2id  14483  sumss  14499  prod2id  14702  fprodfac  14747  strfvi  15960  xpsc0  16267  xpsc1  16268  grpinvfvi  17510  mulgfvi  17592  efgrcl  18174  efgval  18176  frgp0  18219  frgpmhm  18224  vrgpf  18227  vrgpinv  18228  frgpupf  18232  frgpup1  18234  frgpup2  18235  frgpup3lem  18236  frgpnabllem1  18322  frgpnabllem2  18323  rlmsca2  19249  ply1basfvi  19659  ply1plusgfvi  19660  psr1sca2  19669  ply1sca2  19672  ply1scl0  19708  ply1scl1  19710  indislem  20852  2ndcctbss  21306  1stcelcls  21312  txindislem  21484  iscau3  23122  iscmet3  23137  ovolctb  23304  itg2splitlem  23560  deg1fvi  23890  deg1invg  23911  dgrle  24044  logfac  24392  ptpconn  31341  dicvscacl  36797  elinlem  38221  brfvid  38296  fvilbd  38298