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=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
Assertion	tendo0cbv	$$⊢O=\left(g\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$

Proof

Step	Hyp	Ref	Expression
1		tendo0cbv.o	$$⊢O=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
2		eqidd	$$⊢f=g\to {\mathrm{I}\upharpoonright }_B={\mathrm{I}\upharpoonright }_B$$
3	2	cbvmptv	$$⊢\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)=\left(g\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
4	1 3	eqtri	$$⊢O=\left(g\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$