Definition df-csb 3875

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

This definition is referenced by:  csb2  3876  csbeq1  3877  csbeq2  3879  csbeq2d  3880  csbeq2dv  3881  cbvcsbw  3884  cbvcsb  3885  cbvcsbv  3886  csbid  3887  csbcow  3889  csbco  3890  csbtt  3891  csbconstg  3893  csbgfi  3894  nfcsb1d  3896  nfcsbd  3899  nfcsbw  3900  csbie  3909  csbied  3910  csbie2g  3914  cbvralcsf  3916  cbvreucsf  3918  cbvrabcsf  3919  csbprc  4384  sbcel12  4386  sbceqg  4387  csbnestgfw  4397  csbnestgf  4402  csbvarg  4409  csbexg  5280  cbvcsbvw2  36195  cbvcsbdavw  36223  cbvcsbdavw2  36224  bj-csbsnlem  36867  bj-csbprc  36874  csbcom2fi  38098