Definition df-csb 3082

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 2986, to prevent ambiguity. Theorem sbcel1g 3100 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3110 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 3081	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1363	. . . . 5 class 𝑦
7	6, 3	wcel 2164	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 2986	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2179	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1364	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3083  csbeq1  3084  cbvcsbw  3085  cbvcsb  3086  csbid  3089  csbco  3091  csbcow  3092  csbtt  3093  sbcel12g  3096  sbceqg  3097  csbeq2  3105  csbeq2d  3106  csbvarg  3109  nfcsb1d  3112  nfcsbd  3117  nfcsbw  3118  csbie2g  3132  csbnestgf  3134  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  csbprc  3493  csbexga  4158  bdccsb  15422