Definition df-csb 3148

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

This definition is referenced by:  csb2  3149  csbeq1  3150  cbvcsbw  3151  cbvcsb  3152  csbid  3155  csbco  3157  csbcow  3158  csbtt  3159  sbcel12g  3162  sbceqg  3163  csbeq2  3171  csbeq2d  3172  csbvarg  3175  nfcsb1d  3178  nfcsbd  3183  nfcsbw  3184  csbie2g  3198  csbnestgf  3200  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  csbprc  3571  csbexga  4256  bdccsb  16800