Definition df-csb 3058

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 2962, to prevent ambiguity. Theorem sbcel1g 3076 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3086 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 3057	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1352	. . . . 5 class 𝑦
7	6, 3	wcel 2148	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 2962	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2163	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1353	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3059  csbeq1  3060  cbvcsbw  3061  cbvcsb  3062  csbid  3065  csbco  3067  csbcow  3068  csbtt  3069  sbcel12g  3072  sbceqg  3073  csbeq2  3081  csbeq2d  3082  csbvarg  3085  nfcsb1d  3088  nfcsbd  3092  nfcsbw  3093  csbie2g  3107  csbnestgf  3109  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  csbprc  3468  csbexga  4131  bdccsb  14582