Theorem fvi 6968

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104   class class class wbr 5149   I cid 5574  Fun wfun 6538  ‘cfv 6544

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552

This theorem is referenced by:  fviss  6969  fvmpti  6998  fvmpt2  7010  fvresi  7174  seqom0g  8460  fodomfi  9329  seqfeq4  14023  fac1  14243  facp1  14244  bcval5  14284  bcn2  14285  ids1  14553  s1val  14554  climshft2  15532  sum2id  15660  sumss  15676  prod2id  15878  fprodfac  15923  strfvi  17129  grpinvfvi  18905  mulgfvi  18994  efgrcl  19626  efgval  19628  frgp0  19671  frgpmhm  19676  vrgpf  19679  vrgpinv  19680  frgpupf  19684  frgpup1  19686  frgpup2  19687  frgpup3lem  19688  frgpnabllem1  19784  frgpnabllem2  19785  rlmsca2  20970  ply1basfvi  21985  ply1plusgfvi  21986  psr1sca2  21995  ply1sca2  21998  ply1scl0OLD  22035  ply1scl1OLD  22038  indislem  22725  2ndcctbss  23181  1stcelcls  23187  txindislem  23359  iscau3  25028  iscmet3  25043  ovolctb  25241  itg2splitlem  25500  deg1fvi  25837  deg1invg  25858  dgrle  25991  logfac  26343  fnpreimac  32161  ptpconn  34520  dicvscacl  40367  elinlem  42653  brfvid  42742  fvilbd  42744