Definition df-csb 3139

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

This definition is referenced by:  csb2  3140  csbeq1  3141  cbvcsbw  3142  cbvcsb  3143  csbid  3146  csbco  3148  csbcow  3149  csbtt  3150  sbcel12g  3153  sbceqg  3154  csbeq2  3162  csbeq2d  3163  csbvarg  3166  nfcsb1d  3169  nfcsbd  3174  nfcsbw  3175  csbie2g  3189  csbnestgf  3191  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  csbprc  3554  csbexga  4238  bdccsb  16630