Definition df-csb 3847

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 4373 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 4366). Theorem sbccsb 4393 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 3846	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1568	. . . . 5 class 𝑦
7	6, 3	wcel 2144	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3738	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2738	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1569	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is used by:  csb2  3848  csbeq1  3849  csbeq2  3851  csbeq2d  3852  csbeq2dv  3853  cbvcsbw  3856  cbvcsb  3857  cbvcsbv  3858  csbid  3859  csbcow  3861  csbco  3862  csbtt  3863  csbconstg  3865  csbgfi  3866  nfcsb1d  3868  nfcsbd  3871  nfcsbw  3872  csbie  3881  csbied  3882  csbie2g  3886  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  csbprc  4366  sbcel12  4368  sbceqg  4369  csbnestgfw  4379  csbnestgf  4384  csbvarg  4391  csbexg  5263  cbvcsbvw2  37062  cbvcsbdavw  37090  cbvcsbdavw2  37091  bj-csbsnlem  37857  bj-csbprc  37864  csbcom2fi  39103