Definition df-bj-proj

Description: Definition of the class projection corresponding to tagged tuples. The expression ( A Proj B ) denotes the projection on the A^th component. (Contributed by BJ, 6-Apr-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	df-bj-proj	$$⊢\left(AProjB\right)=\left\{x|\left\{x\right\}\in B\left[\left\{A\right\}\right]\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	bj-cproj	$$class\left(AProjB\right)$$
3		vx	$$setvarx$$
4	3	cv	$$setvarx$$
5	4	csn	$$class\left\{x\right\}$$
6	0	csn	$$class\left\{A\right\}$$
7	1 6	cima	$$classB\left[\left\{A\right\}\right]$$
8	5 7	wcel	$$wff\left\{x\right\}\in B\left[\left\{A\right\}\right]$$
9	8 3	cab	$$class\left\{x|\left\{x\right\}\in B\left[\left\{A\right\}\right]\right\}$$
10	2 9	wceq	$$wff\left(AProjB\right)=\left\{x|\left\{x\right\}\in B\left[\left\{A\right\}\right]\right\}$$