Metamath Proof Explorer


Theorem bj-pr2eq

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

Ref Expression
Assertion bj-pr2eq ( 𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵 )

Proof

Step Hyp Ref Expression
1 bj-projeq2 ( 𝐴 = 𝐵 → ( 1o Proj 𝐴 ) = ( 1o Proj 𝐵 ) )
2 df-bj-pr2 pr2 𝐴 = ( 1o Proj 𝐴 )
3 df-bj-pr2 pr2 𝐵 = ( 1o Proj 𝐵 )
4 1 2 3 3eqtr4g ( 𝐴 = 𝐵 → pr2 𝐴 = pr2 𝐵 )