Definition df-csb 3534

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 3435, to prevent ambiguity. Theorem sbcel1g 3987 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 4004 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 3533	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1482	. . . . 5 class 𝑦
7	6, 3	wcel 1990	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3435	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2608	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1483	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3535  csbeq1  3536  csbeq2  3537  cbvcsb  3538  csbid  3541  csbco  3543  csbtt  3544  nfcsb1d  3547  nfcsbd  3550  csbie2g  3564  cbvralcsf  3565  cbvreucsf  3567  cbvrabcsf  3568  csbprc  3980  csbprcOLD  3981  sbcel12  3983  sbceqg  3984  csbeq2d  3991  csbnestgf  3996  csbvarg  4003  csbexg  4792  bj-csbsnlem  32898  bj-csbprc  32904  csbcom2fi  33934  csbgfi  33935  sbcel12gOLD  38754