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	|- ( A Proj B ) = { x | { x } e. ( B " { A } ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	bj-cproj	|- ( A Proj B )
3		vx	|- x
4	3	cv	|- x
5	4	csn	|- { x }
6	0	csn	|- { A }
7	1 6	cima	|- ( B " { A } )
8	5 7	wcel	|- { x } e. ( B " { A } )
9	8 3	cab	|- { x | { x } e. ( B " { A } ) }
10	2 9	wceq	|- ( A Proj B ) = { x | { x } e. ( B " { A } ) }