Definition df-csb 3853

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 3743, to prevent ambiguity. Theorem sbcel1g 4380 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 4373). Theorem sbccsb 4400 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 3852	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1567	. . . . 5 class 𝑦
7	6, 3	wcel 2141	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3743	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2739	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1568	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3854  csbeq1  3855  csbeq2  3857  csbeq2d  3858  csbeq2dv  3859  cbvcsbw  3862  cbvcsb  3863  cbvcsbv  3864  csbid  3865  csbcow  3867  csbco  3868  csbtt  3869  csbconstg  3871  csbgfi  3872  nfcsb1d  3874  nfcsbd  3877  nfcsbw  3878  csbie  3887  csbied  3888  csbie2g  3892  cbvralcsf  3894  cbvreucsf  3896  cbvrabcsf  3897  csbprc  4373  sbcel12  4375  sbceqg  4376  csbnestgfw  4386  csbnestgf  4391  csbvarg  4398  csbexg  5272  cbvcsbvw2  36687  cbvcsbdavw  36715  cbvcsbdavw2  36716  bj-csbsnlem  37482  bj-csbprc  37489  csbcom2fi  38723