Metamath Proof Explorer


Definition df-bj-pr2

Description: Definition of the second projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr2eq , bj-pr22val , bj-pr2ex . (Contributed by BJ, 6-Oct-2018) (New usage is discouraged.)

Ref Expression
Assertion df-bj-pr2 pr2 𝐴 = ( 1o Proj 𝐴 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 0 bj-cpr2 pr2 𝐴
2 c1o 1o
3 2 0 bj-cproj ( 1o Proj 𝐴 )
4 1 3 wceq pr2 𝐴 = ( 1o Proj 𝐴 )