Definition df-csb 3126

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

This definition is referenced by:  csb2  3127  csbeq1  3128  cbvcsbw  3129  cbvcsb  3130  csbid  3133  csbco  3135  csbcow  3136  csbtt  3137  sbcel12g  3140  sbceqg  3141  csbeq2  3149  csbeq2d  3150  csbvarg  3153  nfcsb1d  3156  nfcsbd  3161  nfcsbw  3162  csbie2g  3176  csbnestgf  3178  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  csbprc  3538  csbexga  4213  bdccsb  16365