Definition df-csb 2909

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 2815, to prevent ambiguity. Theorem sbcel1g 2925 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2934 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 2908	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1283	. . . . 5 class 𝑦
7	6, 3	wcel 1433	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 2815	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2067	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1284	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  2910  csbeq1  2911  cbvcsb  2912  csbid  2915  csbco  2917  csbtt  2918  sbcel12g  2921  sbceqg  2922  csbeq2d  2930  csbvarg  2933  nfcsb1d  2936  nfcsbd  2939  csbie2g  2952  csbnestgf  2954  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  csbprc  3289  csbexga  3906  bdccsb  10651