Definition df-bj-pr1

Description: Definition of the first projection of a class tuple. New usage is discouraged because the precise definition is generally unimportant compared to the characteristic properties bj-pr1eq , bj-pr11val , bj-pr21val , bj-pr1ex . (Contributed by BJ, 6-Apr-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	df-bj-pr1	$$⊢pr1A=\left(\varnothing ProjA\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	bj-cpr1	$$classpr1A$$
2		c0	$$class\varnothing$$
3	2 0	bj-cproj	$$class\left(\varnothing ProjA\right)$$
4	1 3	wceq	$$wffpr1A=\left(\varnothing ProjA\right)$$