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 4366 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 4359). Theorem sbccsb 4386 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 1540	. . . . 5 class 𝑦
7	6, 3	wcel 2113	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3738	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2712	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1541	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  4359  sbcel12  4361  sbceqg  4362  csbnestgfw  4372  csbnestgf  4377  csbvarg  4384  csbexg  5253  cbvcsbvw2  36374  cbvcsbdavw  36402  cbvcsbdavw2  36403  bj-csbsnlem  37047  bj-csbprc  37054  csbcom2fi  38268