Definition df-csb 3096

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 3000, to prevent ambiguity. Theorem sbcel1g 3114 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3124 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 3095	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1372	. . . . 5 class 𝑦
7	6, 3	wcel 2177	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3000	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2192	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1373	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3097  csbeq1  3098  cbvcsbw  3099  cbvcsb  3100  csbid  3103  csbco  3105  csbcow  3106  csbtt  3107  sbcel12g  3110  sbceqg  3111  csbeq2  3119  csbeq2d  3120  csbvarg  3123  nfcsb1d  3126  nfcsbd  3131  nfcsbw  3132  csbie2g  3146  csbnestgf  3148  cbvralcsf  3158  cbvrexcsf  3159  cbvreucsf  3160  cbvrabcsf  3161  csbprc  3508  csbexga  4177  bdccsb  15910