Definition df-bj-proj 32979

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.)

Assertion

Ref	Expression
df-bj-proj	|- ( A Proj B ) = { x | { x } e. ( B " { A } ) }

Distinct variable groups:   x, A   x, B

Detailed syntax breakdown of Definition df-bj-proj

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	bj-cproj 32978	. 2 class ( A Proj B )
4		vx	. . . . . 6 setvar x
5	4	cv 1482	. . . . 5 class x
6	5	csn 4177	. . . 4 class { x }
7	1	csn 4177	. . . . 5 class { A }
8	2, 7	cima 5117	. . . 4 class ( B " { A } )
9	6, 8	wcel 1990	. . 3 wff { x } e. ( B " { A } )
10	9, 4	cab 2608	. 2 class { x | { x } e. ( B " { A } ) }
11	3, 10	wceq 1483	1 wff ( A Proj B ) = { x | { x } e. ( B " { A } ) }

This definition is referenced by:  bj-projeq  32980  bj-projun  32982  bj-projex  32983  bj-projval  32984