Definition df-csb 3855

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 3746, to prevent ambiguity. Theorem sbcel1g 4372 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 4365). Theorem sbccsb 4392 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 3854	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1561	. . . . 5 class 𝑦
7	6, 3	wcel 2144	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3746	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2742	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1562	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3856  csbeq1  3857  csbeq2  3859  csbeq2d  3860  csbeq2dv  3861  cbvcsbw  3864  cbvcsb  3865  cbvcsbv  3866  csbid  3867  csbcow  3869  csbco  3870  csbtt  3871  csbconstg  3873  csbgfi  3874  nfcsb1d  3876  nfcsbd  3879  nfcsbw  3880  csbie  3889  csbied  3890  csbie2g  3894  cbvralcsf  3896  cbvreucsf  3898  cbvrabcsf  3899  csbprc  4365  sbcel12  4367  sbceqg  4368  csbnestgfw  4378  csbnestgf  4383  csbvarg  4390  csbexg  5262  cbvcsbvw2  36596  cbvcsbdavw  36624  cbvcsbdavw2  36625  bj-csbsnlem  37393  bj-csbprc  37400  csbcom2fi  38632