Theorem tendo0cbv

Description: Define additive identity for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypothesis	tendo0cbv.o	|- O = ( f e. T |-> ( _I |` B ) )
Assertion	tendo0cbv	|- O = ( g e. T |-> ( _I |` B ) )

Proof

Step	Hyp	Ref	Expression
1		tendo0cbv.o	|- O = ( f e. T |-> ( _I |` B ) )
2		eqidd	|- ( f = g -> ( _I |` B ) = ( _I |` B ) )
3	2	cbvmptv	|- ( f e. T |-> ( _I |` B ) ) = ( g e. T |-> ( _I |` B ) )
4	1 3	eqtri	|- O = ( g e. T |-> ( _I |` B ) )