Definition df-bj-proj 37014

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

Assertion

Ref	Expression
df-bj-proj	⊢ (𝐴 Proj 𝐵) = {𝑥 ∣ {𝑥} ∈ (𝐵 “ {𝐴})}

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Detailed syntax breakdown of Definition df-bj-proj

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	bj-cproj 37013	. 2 class (𝐴 Proj 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1539	. . . . 5 class 𝑥
6	5	csn 4606	. . . 4 class {𝑥}
7	1	csn 4606	. . . . 5 class {𝐴}
8	2, 7	cima 5662	. . . 4 class (𝐵 “ {𝐴})
9	6, 8	wcel 2109	. . 3 wff {𝑥} ∈ (𝐵 “ {𝐴})
10	9, 4	cab 2714	. 2 class {𝑥 ∣ {𝑥} ∈ (𝐵 “ {𝐴})}
11	3, 10	wceq 1540	1 wff (𝐴 Proj 𝐵) = {𝑥 ∣ {𝑥} ∈ (𝐵 “ {𝐴})}

This definition is referenced by:  bj-projeq  37015  bj-projun  37017  bj-projex  37018  bj-projval  37019