Theorem fvi 6940

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 6551	. 2 ⊢ Fun I
2		ididg 5820	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 I 𝐴)
3		funbrfv 6912	. 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 5110   I cid 5535  Fun wfun 6508  ‘cfv 6514

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522

This theorem is referenced by:  fviss  6941  fvmpti  6970  fvmpt2  6982  fvresi  7150  seqom0g  8427  fodomfi  9268  fodomfiOLD  9288  seqfeq4  14023  fac1  14249  facp1  14250  bcval5  14290  bcn2  14291  ids1  14569  s1val  14570  climshft2  15555  sum2id  15681  sumss  15697  prod2id  15901  fprodfac  15946  strfvi  17167  grpinvfvi  18921  mulgfvi  19012  efgrcl  19652  efgval  19654  frgp0  19697  frgpmhm  19702  vrgpf  19705  vrgpinv  19706  frgpupf  19710  frgpup1  19712  frgpup2  19713  frgpup3lem  19714  frgpnabllem1  19810  frgpnabllem2  19811  rlmsca2  21113  ply1basfvi  22132  ply1plusgfvi  22133  psr1sca2  22142  ply1sca2  22145  ply1scl0OLD  22184  ply1scl1OLD  22187  indislem  22894  2ndcctbss  23349  1stcelcls  23355  txindislem  23527  iscau3  25185  iscmet3  25200  ovolctb  25398  itg2splitlem  25656  deg1fvi  25997  deg1invg  26018  dgrle  26155  logfac  26517  fnpreimac  32602  ptpconn  35227  dicvscacl  41192  elinlem  43594  brfvid  43683  fvilbd  43685  nregmodelf1o  45012  tposid  48877  tposidres  48878