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 4381 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 4374). Theorem sbccsb 4401 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 1569	. . . . 5 class 𝑦
7	6, 3	wcel 2143	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3744	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2741	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1570	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is used 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  4374  sbcel12  4376  sbceqg  4377  csbnestgfw  4387  csbnestgf  4392  csbvarg  4399  csbexg  5273  cbvcsbvw2  36771  cbvcsbdavw  36799  cbvcsbdavw2  36800  bj-csbsnlem  37566  bj-csbprc  37573  csbcom2fi  38805