Definition df-csb 3004

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

This definition is referenced by:  csb2  3005  csbeq1  3006  cbvcsbw  3007  cbvcsb  3008  csbid  3011  csbco  3013  csbtt  3014  sbcel12g  3017  sbceqg  3018  csbeq2  3026  csbeq2d  3027  csbvarg  3030  nfcsb1d  3033  nfcsbd  3036  csbie2g  3050  csbnestgf  3052  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  csbprc  3408  csbexga  4056  bdccsb  13058