Definition df-csb 3852

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 3742, to prevent ambiguity. Theorem sbcel1g 4377 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 4370). Theorem sbccsb 4397 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 3851	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1569	. . . . 5 class 𝑦
7	6, 3	wcel 2147	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3742	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2741	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1570	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is used by:  csb2  3853  csbeq1  3854  csbeq2  3856  csbeq2d  3857  csbeq2dv  3858  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbid  3864  csbcow  3866  csbco  3867  csbtt  3868  csbconstg  3870  csbgfi  3871  nfcsb1d  3873  nfcsbd  3876  nfcsbw  3877  csbie  3886  csbied  3887  csbie2g  3891  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  csbprc  4370  sbcel12  4372  sbceqg  4373  csbnestgfw  4383  csbnestgf  4388  csbvarg  4395  csbexg  5267  cbvcsbvw2  37197  cbvcsbdavw  37225  cbvcsbdavw2  37226  bj-csbsnlem  37992  bj-csbprc  37999  csbcom2fi  39251