Definition df-csb 3142

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

This definition is referenced by:  csb2  3143  csbeq1  3144  cbvcsbw  3145  cbvcsb  3146  csbid  3149  csbco  3151  csbcow  3152  csbtt  3153  sbcel12g  3156  sbceqg  3157  csbeq2  3165  csbeq2d  3166  csbvarg  3169  nfcsb1d  3172  nfcsbd  3177  nfcsbw  3178  csbie2g  3192  csbnestgf  3194  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  csbprc  3558  csbexga  4243  bdccsb  16756