Theorem bj-projeq2

Description: Substitution property for Proj . (Contributed by BJ, 6-Apr-2019)

	Ref	Expression
Assertion	bj-projeq2	⊢ ( 𝐵 = 𝐶 → ( 𝐴 Proj 𝐵 ) = ( 𝐴 Proj 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ 𝐴 = 𝐴
2		bj-projeq	⊢ ( 𝐴 = 𝐴 → ( 𝐵 = 𝐶 → ( 𝐴 Proj 𝐵 ) = ( 𝐴 Proj 𝐶 ) ) )
3	1 2	ax-mp	⊢ ( 𝐵 = 𝐶 → ( 𝐴 Proj 𝐵 ) = ( 𝐴 Proj 𝐶 ) )