Definition df-csb 3854

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

This definition is referenced by:  csb2  3855  csbeq1  3856  csbeq2  3858  csbeq2d  3859  csbeq2dv  3860  cbvcsbw  3863  cbvcsb  3864  cbvcsbv  3865  csbid  3866  csbcow  3868  csbco  3869  csbtt  3870  csbconstg  3872  csbgfi  3873  nfcsb1d  3875  nfcsbd  3878  nfcsbw  3879  csbie  3888  csbied  3889  csbie2g  3893  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  csbprc  4362  sbcel12  4364  sbceqg  4365  csbnestgfw  4375  csbnestgf  4380  csbvarg  4387  csbexg  5252  cbvcsbvw2  36207  cbvcsbdavw  36235  cbvcsbdavw2  36236  bj-csbsnlem  36879  bj-csbprc  36886  csbcom2fi  38110