Definition df-csb 3129

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 3032, to prevent ambiguity. Theorem sbcel1g 3147 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3157 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 3128	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1397	. . . . 5 class 𝑦
7	6, 3	wcel 2202	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3032	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2217	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1398	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3130  csbeq1  3131  cbvcsbw  3132  cbvcsb  3133  csbid  3136  csbco  3138  csbcow  3139  csbtt  3140  sbcel12g  3143  sbceqg  3144  csbeq2  3152  csbeq2d  3153  csbvarg  3156  nfcsb1d  3159  nfcsbd  3164  nfcsbw  3165  csbie2g  3179  csbnestgf  3181  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  csbprc  3542  csbexga  4222  bdccsb  16576