Definition df-csb 3851

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 3850	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1569	. . . . 5 class 𝑦
7	6, 3	wcel 2145	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3742	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2740	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1570	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is used by:  csb2  3852  csbeq1  3853  csbeq2  3855  csbeq2d  3856  csbeq2dv  3857  cbvcsbw  3860  cbvcsb  3861  cbvcsbv  3862  csbid  3863  csbcow  3865  csbco  3866  csbtt  3867  csbconstg  3869  csbgfi  3870  nfcsb1d  3872  nfcsbd  3875  nfcsbw  3876  csbie  3885  csbied  3886  csbie2g  3890  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  csbprc  4370  sbcel12  4372  sbceqg  4373  csbnestgfw  4383  csbnestgf  4388  csbvarg  4395  csbexg  5271  cbvcsbvw2  36838  cbvcsbdavw  36866  cbvcsbdavw2  36867  bj-csbsnlem  37633  bj-csbprc  37640  csbcom2fi  38863