Definition df-csb 3128

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

This definition is referenced by:  csb2  3129  csbeq1  3130  cbvcsbw  3131  cbvcsb  3132  csbid  3135  csbco  3137  csbcow  3138  csbtt  3139  sbcel12g  3142  sbceqg  3143  csbeq2  3151  csbeq2d  3152  csbvarg  3155  nfcsb1d  3158  nfcsbd  3163  nfcsbw  3164  csbie2g  3178  csbnestgf  3180  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  csbprc  3540  csbexga  4217  bdccsb  16455