Definition df-csb 3499

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 3401, to prevent ambiguity. Theorem sbcel1g 3938 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3955 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 3498	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1473	. . . . 5 class 𝑦
7	6, 3	wcel 1976	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3401	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2595	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1474	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3500  csbeq1  3501  csbeq2  3502  cbvcsb  3503  csbid  3506  csbco  3508  csbtt  3509  nfcsb1d  3512  nfcsbd  3515  csbie2g  3529  cbvralcsf  3530  cbvreucsf  3532  cbvrabcsf  3533  csbprc  3931  csbprcOLD  3932  sbcel12  3934  sbceqg  3935  csbeq2d  3942  csbnestgf  3947  csbvarg  3954  csbexg  4714  bj-csbsnlem  31873  bj-csbprc  31879  csbcom2fi  32887  csbgfi  32888  sbcel12gOLD  37558