Definition df-csb 3567

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 3468, to prevent ambiguity. Theorem sbcel1g 4020 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 4037 recreates 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 3566	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1522	. . . . 5 class 𝑦
7	6, 3	wcel 2030	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3468	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2637	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1523	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3568  csbeq1  3569  csbeq2  3570  cbvcsb  3571  csbid  3574  csbco  3576  csbtt  3577  nfcsb1d  3580  nfcsbd  3583  csbie2g  3597  cbvralcsf  3598  cbvreucsf  3600  cbvrabcsf  3601  csbprc  4013  csbprcOLD  4014  sbcel12  4016  sbceqg  4017  csbeq2d  4024  csbnestgf  4029  csbvarg  4036  csbexg  4825  bj-csbsnlem  33023  bj-csbprc  33029  csbcom2fi  34064  csbgfi  34065  sbcel12gOLD  39071