Definition df-csb 3908

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 3790, to prevent ambiguity. Theorem sbcel1g 4421 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 4414). Theorem sbccsb 4441 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 3907	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1535	. . . . 5 class 𝑦
7	6, 3	wcel 2105	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3790	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2711	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1536	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3909  csbeq1  3910  csbeq2  3912  csbeq2d  3913  csbeq2dv  3914  cbvcsbw  3917  cbvcsb  3918  cbvcsbv  3919  csbid  3920  csbcow  3922  csbco  3923  csbtt  3924  csbconstg  3926  csbgfi  3928  nfcsb1d  3930  nfcsbd  3933  nfcsbw  3934  csbie  3943  csbied  3945  csbie2g  3950  cbvralcsf  3952  cbvreucsf  3954  cbvrabcsf  3955  csbprc  4414  sbcel12  4416  sbceqg  4417  csbnestgfw  4427  csbnestgf  4432  csbvarg  4439  csbexg  5315  cbvcsbvw2  36213  cbvcsbdavw  36241  cbvcsbdavw2  36242  bj-csbsnlem  36885  bj-csbprc  36892  csbcom2fi  38114