Theorem fvi 6955

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   class class class wbr 5119   I cid 5547  Fun wfun 6525  ‘cfv 6531

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539

This theorem is referenced by:  fviss  6956  fvmpti  6985  fvmpt2  6997  fvresi  7165  seqom0g  8470  fodomfi  9322  fodomfiOLD  9342  seqfeq4  14069  fac1  14295  facp1  14296  bcval5  14336  bcn2  14337  ids1  14615  s1val  14616  climshft2  15598  sum2id  15724  sumss  15740  prod2id  15944  fprodfac  15989  strfvi  17209  grpinvfvi  18965  mulgfvi  19056  efgrcl  19696  efgval  19698  frgp0  19741  frgpmhm  19746  vrgpf  19749  vrgpinv  19750  frgpupf  19754  frgpup1  19756  frgpup2  19757  frgpup3lem  19758  frgpnabllem1  19854  frgpnabllem2  19855  rlmsca2  21157  ply1basfvi  22176  ply1plusgfvi  22177  psr1sca2  22186  ply1sca2  22189  ply1scl0OLD  22228  ply1scl1OLD  22231  indislem  22938  2ndcctbss  23393  1stcelcls  23399  txindislem  23571  iscau3  25230  iscmet3  25245  ovolctb  25443  itg2splitlem  25701  deg1fvi  26042  deg1invg  26063  dgrle  26200  logfac  26562  fnpreimac  32649  ptpconn  35255  dicvscacl  41210  elinlem  43622  brfvid  43711  fvilbd  43713  tposid  48860  tposidres  48861