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	$$⊢pr2A=\left(1_{𝑜}ProjA\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	bj-cpr2	$$classpr2A$$
2		c1o	$$class{1}_{𝑜}$$
3	2 0	bj-cproj	$$class\left(1_{𝑜}ProjA\right)$$
4	1 3	wceq	$$wffpr2A=\left(1_{𝑜}ProjA\right)$$