Definition df-csb 3863

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 3753, to prevent ambiguity. Theorem sbcel1g 4379 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 4372). Theorem sbccsb 4399 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 3862	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1539	. . . . 5 class 𝑦
7	6, 3	wcel 2109	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3753	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2707	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1540	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3864  csbeq1  3865  csbeq2  3867  csbeq2d  3868  csbeq2dv  3869  cbvcsbw  3872  cbvcsb  3873  cbvcsbv  3874  csbid  3875  csbcow  3877  csbco  3878  csbtt  3879  csbconstg  3881  csbgfi  3882  nfcsb1d  3884  nfcsbd  3887  nfcsbw  3888  csbie  3897  csbied  3898  csbie2g  3902  cbvralcsf  3904  cbvreucsf  3906  cbvrabcsf  3907  csbprc  4372  sbcel12  4374  sbceqg  4375  csbnestgfw  4385  csbnestgf  4390  csbvarg  4397  csbexg  5265  cbvcsbvw2  36219  cbvcsbdavw  36247  cbvcsbdavw2  36248  bj-csbsnlem  36891  bj-csbprc  36898  csbcom2fi  38122