Theorem fvi 6937

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 6548	. 2 ⊢ Fun I
2		ididg 5817	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
3		funbrfv 6909	. 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 5107   I cid 5532  Fun wfun 6505  ‘cfv 6511

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  fviss  6938  fvmpti  6967  fvmpt2  6979  fvresi  7147  seqom0g  8424  fodomfi  9261  fodomfiOLD  9281  seqfeq4  14016  fac1  14242  facp1  14243  bcval5  14283  bcn2  14284  ids1  14562  s1val  14563  climshft2  15548  sum2id  15674  sumss  15690  prod2id  15894  fprodfac  15939  strfvi  17160  grpinvfvi  18914  mulgfvi  19005  efgrcl  19645  efgval  19647  frgp0  19690  frgpmhm  19695  vrgpf  19698  vrgpinv  19699  frgpupf  19703  frgpup1  19705  frgpup2  19706  frgpup3lem  19707  frgpnabllem1  19803  frgpnabllem2  19804  rlmsca2  21106  ply1basfvi  22125  ply1plusgfvi  22126  psr1sca2  22135  ply1sca2  22138  ply1scl0OLD  22177  ply1scl1OLD  22180  indislem  22887  2ndcctbss  23342  1stcelcls  23348  txindislem  23520  iscau3  25178  iscmet3  25193  ovolctb  25391  itg2splitlem  25649  deg1fvi  25990  deg1invg  26011  dgrle  26148  logfac  26510  fnpreimac  32595  ptpconn  35220  dicvscacl  41185  elinlem  43587  brfvid  43676  fvilbd  43678  nregmodelf1o  45005  cjnpoly  46890  tposid  48873  tposidres  48874