Definition df-csb 3780

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 3674, to prevent ambiguity. Theorem sbcel1g 4245 shows an example of how ambiguity could arise if we did not use distinguished brackets. When 𝐴 is a proper class, this evaluates to the empty set (see csbprc 4238). Theorem sbccsb 4263 recovers 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 3779	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1507	. . . . 5 class 𝑦
7	6, 3	wcel 2051	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3674	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2751	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1508	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3781  csbeq1  3782  csbeq2  3783  cbvcsb  3784  csbid  3787  csbco  3789  csbtt  3790  csbgfi  3793  nfcsb1d  3795  nfcsbd  3798  csbie2g  3812  cbvralcsf  3813  cbvreucsf  3815  cbvrabcsf  3816  csbprc  4238  sbcel12  4240  sbceqg  4241  csbeq2d  4249  csbnestgf  4254  csbvarg  4261  csbexg  5067  bj-csbsnlem  33749  bj-csbprc  33755  csbcom2fi  34887