Definition df-csb 3846

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 3736, to prevent ambiguity. Theorem sbcel1g 4363 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 4356). Theorem sbccsb 4383 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 3845	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1540	. . . . 5 class 𝑦
7	6, 3	wcel 2111	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3736	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2709	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1541	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3847  csbeq1  3848  csbeq2  3850  csbeq2d  3851  csbeq2dv  3852  cbvcsbw  3855  cbvcsb  3856  cbvcsbv  3857  csbid  3858  csbcow  3860  csbco  3861  csbtt  3862  csbconstg  3864  csbgfi  3865  nfcsb1d  3867  nfcsbd  3870  nfcsbw  3871  csbie  3880  csbied  3881  csbie2g  3885  cbvralcsf  3887  cbvreucsf  3889  cbvrabcsf  3890  csbprc  4356  sbcel12  4358  sbceqg  4359  csbnestgfw  4369  csbnestgf  4374  csbvarg  4381  csbexg  5246  cbvcsbvw2  36273  cbvcsbdavw  36301  cbvcsbdavw2  36302  bj-csbsnlem  36945  bj-csbprc  36952  csbcom2fi  38176