Definition df-csb 3050

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 2955, to prevent ambiguity. Theorem sbcel1g 3068 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3078 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 3049	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1347	. . . . 5 class 𝑦
7	6, 3	wcel 2141	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 2955	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2156	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1348	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3051  csbeq1  3052  cbvcsbw  3053  cbvcsb  3054  csbid  3057  csbco  3059  csbcow  3060  csbtt  3061  sbcel12g  3064  sbceqg  3065  csbeq2  3073  csbeq2d  3074  csbvarg  3077  nfcsb1d  3080  nfcsbd  3084  nfcsbw  3085  csbie2g  3099  csbnestgf  3101  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  csbprc  3460  csbexga  4117  bdccsb  13895