Definition df-csb 3008

Description: Define the proper substitution of a class for a set into another class. The underlined brackets distinguish it from the substitution into a wff, wsbc 2913, to prevent ambiguity. Theorem sbcel1g 3026 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3036 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
df-csb	⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-csb

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	csb 3007	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1331	. . . . 5 class 𝑦
7	6, 3	wcel 1481	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 2913	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2126	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1332	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3009  csbeq1  3010  cbvcsbw  3011  cbvcsb  3012  csbid  3015  csbco  3017  csbtt  3019  sbcel12g  3022  sbceqg  3023  csbeq2  3031  csbeq2d  3032  csbvarg  3035  nfcsb1d  3038  nfcsbd  3041  csbie2g  3055  csbnestgf  3057  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  csbprc  3413  csbexga  4064  bdccsb  13229