Theorem bj-pr2eq

Description: Substitution property for pr2 . (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-pr2eq	|- ( A = B -> pr2 A = pr2 B )

Proof

Step	Hyp	Ref	Expression
1		bj-projeq2	|- ( A = B -> ( 1o Proj A ) = ( 1o Proj B ) )
2		df-bj-pr2	|- pr2 A = ( 1o Proj A )
3		df-bj-pr2	|- pr2 B = ( 1o Proj B )
4	1 2 3	3eqtr4g	|- ( A = B -> pr2 A = pr2 B )