Definition df-bj-proj 35108

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 35107	. 2 class (𝐴 Proj 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1538	. . . . 5 class 𝑥
6	5	csn 4558	. . . 4 class {𝑥}
7	1	csn 4558	. . . . 5 class {𝐴}
8	2, 7	cima 5583	. . . 4 class (𝐵 “ {𝐴})
9	6, 8	wcel 2108	. . 3 wff {𝑥} ∈ (𝐵 “ {𝐴})
10	9, 4	cab 2715	. 2 class {𝑥 ∣ {𝑥} ∈ (𝐵 “ {𝐴})}
11	3, 10	wceq 1539	1 wff (𝐴 Proj 𝐵) = {𝑥 ∣ {𝑥} ∈ (𝐵 “ {𝐴})}

This definition is referenced by:  bj-projeq  35109  bj-projun  35111  bj-projex  35112  bj-projval  35113