Definition df-csb 3848

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 3738, to prevent ambiguity. Theorem sbcel1g 4363 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 4356). Theorem sbccsb 4383 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 3847	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1539	. . . . 5 class 𝑦
7	6, 3	wcel 2109	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3738	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2707	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1540	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3849  csbeq1  3850  csbeq2  3852  csbeq2d  3853  csbeq2dv  3854  cbvcsbw  3857  cbvcsb  3858  cbvcsbv  3859  csbid  3860  csbcow  3862  csbco  3863  csbtt  3864  csbconstg  3866  csbgfi  3867  nfcsb1d  3869  nfcsbd  3872  nfcsbw  3873  csbie  3882  csbied  3883  csbie2g  3887  cbvralcsf  3889  cbvreucsf  3891  cbvrabcsf  3892  csbprc  4356  sbcel12  4358  sbceqg  4359  csbnestgfw  4369  csbnestgf  4374  csbvarg  4381  csbexg  5245  cbvcsbvw2  36222  cbvcsbdavw  36250  cbvcsbdavw2  36251  bj-csbsnlem  36894  bj-csbprc  36901  csbcom2fi  38125