Definition df-csb 3125

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 3028, to prevent ambiguity. Theorem sbcel1g 3143 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3153 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 3124	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1394	. . . . 5 class 𝑦
7	6, 3	wcel 2200	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3028	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2215	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1395	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3126  csbeq1  3127  cbvcsbw  3128  cbvcsb  3129  csbid  3132  csbco  3134  csbcow  3135  csbtt  3136  sbcel12g  3139  sbceqg  3140  csbeq2  3148  csbeq2d  3149  csbvarg  3152  nfcsb1d  3155  nfcsbd  3160  nfcsbw  3161  csbie2g  3175  csbnestgf  3177  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  csbprc  3537  csbexga  4211  bdccsb  16153