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 3741, to prevent ambiguity. Theorem sbcel1g 4369 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 4362). Theorem sbccsb 4389 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 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2114	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3741	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2715	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced 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  4362  sbcel12  4364  sbceqg  4365  csbnestgfw  4375  csbnestgf  4380  csbvarg  4387  csbexg  5256  cbvcsbvw2  36427  cbvcsbdavw  36455  cbvcsbdavw2  36456  bj-csbsnlem  37106  bj-csbprc  37113  csbcom2fi  38331