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	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion	tendo0cbv	⊢ 𝑂 = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		tendo0cbv.o	⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
2		eqidd	⊢ ( 𝑓 = 𝑔 → ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) )
3	2	cbvmptv	⊢ ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
4	1 3	eqtri	⊢ 𝑂 = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )