Definition df-csb 3070

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

This definition is referenced by:  csb2  3071  csbeq1  3072  cbvcsbw  3073  cbvcsb  3074  csbid  3077  csbco  3079  csbcow  3080  csbtt  3081  sbcel12g  3084  sbceqg  3085  csbeq2  3093  csbeq2d  3094  csbvarg  3097  nfcsb1d  3100  nfcsbd  3104  nfcsbw  3105  csbie2g  3119  csbnestgf  3121  cbvralcsf  3131  cbvrexcsf  3132  cbvreucsf  3133  cbvrabcsf  3134  csbprc  3480  csbexga  4143  bdccsb  14883