Metamath Proof Explorer


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 1 𝑜 Proj A = 1 𝑜 Proj B
2 df-bj-pr2 pr2 A = 1 𝑜 Proj A
3 df-bj-pr2 pr2 B = 1 𝑜 Proj B
4 1 2 3 3eqtr4g A = B pr2 A = pr2 B