Theorem bj-projeq2

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

	Ref	Expression
Assertion	bj-projeq2	$$⊢B=C\to \left(AProjB\right)=\left(AProjC\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A=A$$
2		bj-projeq	$$⊢A=A\to \left(B=C\to \left(AProjB\right)=\left(AProjC\right)\right)$$
3	1 2	ax-mp	$$⊢B=C\to \left(AProjB\right)=\left(AProjC\right)$$