Definition df-csb 3833

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 3716, to prevent ambiguity. Theorem sbcel1g 4347 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 4340). Theorem sbccsb 4367 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 3832	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1538	. . . . 5 class 𝑦
7	6, 3	wcel 2106	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3716	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2715	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1539	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3834  csbeq1  3835  csbeq2  3837  csbeq2d  3838  cbvcsbw  3842  cbvcsb  3843  csbid  3845  csbcow  3847  csbco  3848  csbtt  3849  csbconstg  3851  csbgfi  3853  nfcsb1d  3855  nfcsbd  3858  nfcsbw  3859  csbie  3868  csbied  3870  csbie2g  3875  cbvralcsf  3877  cbvreucsf  3879  cbvrabcsf  3880  csbprc  4340  sbcel12  4342  sbceqg  4343  csbnestgfw  4353  csbnestgf  4358  csbvarg  4365  csbexg  5234  bj-csbsnlem  35088  bj-csbprc  35095  csbcom2fi  36286