Definition df-csb 3852

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 4370 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 4363). Theorem sbccsb 4390 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 3851	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2114	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3742	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2715	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3853  csbeq1  3854  csbeq2  3856  csbeq2d  3857  csbeq2dv  3858  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbid  3864  csbcow  3866  csbco  3867  csbtt  3868  csbconstg  3870  csbgfi  3871  nfcsb1d  3873  nfcsbd  3876  nfcsbw  3877  csbie  3886  csbied  3887  csbie2g  3891  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  csbprc  4363  sbcel12  4365  sbceqg  4366  csbnestgfw  4376  csbnestgf  4381  csbvarg  4388  csbexg  5259  cbvcsbvw2  36453  cbvcsbdavw  36481  cbvcsbdavw2  36482  bj-csbsnlem  37178  bj-csbprc  37185  csbcom2fi  38408