Definition df-csb 3045

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 2950, to prevent ambiguity. Theorem sbcel1g 3063 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3073 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 3044	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1342	. . . . 5 class 𝑦
7	6, 3	wcel 2136	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 2950	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2151	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1343	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3046  csbeq1  3047  cbvcsbw  3048  cbvcsb  3049  csbid  3052  csbco  3054  csbcow  3055  csbtt  3056  sbcel12g  3059  sbceqg  3060  csbeq2  3068  csbeq2d  3069  csbvarg  3072  nfcsb1d  3075  nfcsbd  3079  nfcsbw  3080  csbie2g  3094  csbnestgf  3096  cbvralcsf  3106  cbvrexcsf  3107  cbvreucsf  3108  cbvrabcsf  3109  csbprc  3453  csbexga  4109  bdccsb  13702