Definition df-csb 3900

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 3788, to prevent ambiguity. Theorem sbcel1g 4416 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 4409). Theorem sbccsb 4436 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 3899	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1539	. . . . 5 class 𝑦
7	6, 3	wcel 2108	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3788	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2714	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1540	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3901  csbeq1  3902  csbeq2  3904  csbeq2d  3905  csbeq2dv  3906  cbvcsbw  3909  cbvcsb  3910  cbvcsbv  3911  csbid  3912  csbcow  3914  csbco  3915  csbtt  3916  csbconstg  3918  csbgfi  3919  nfcsb1d  3921  nfcsbd  3924  nfcsbw  3925  csbie  3934  csbied  3935  csbie2g  3939  cbvralcsf  3941  cbvreucsf  3943  cbvrabcsf  3944  csbprc  4409  sbcel12  4411  sbceqg  4412  csbnestgfw  4422  csbnestgf  4427  csbvarg  4434  csbexg  5310  cbvcsbvw2  36232  cbvcsbdavw  36260  cbvcsbdavw2  36261  bj-csbsnlem  36904  bj-csbprc  36911  csbcom2fi  38135