Definition df-csb 2853

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 2764, to prevent ambiguity. Theorem sbcel1g 2869 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2878 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 2852	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1242	. . . . 5 class 𝑦
7	6, 3	wcel 1393	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 2764	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2026	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1243	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  2854  csbeq1  2855  cbvcsb  2856  csbid  2859  csbco  2861  csbtt  2862  sbcel12g  2865  sbceqg  2866  csbeq2d  2874  csbvarg  2877  nfcsb1d  2880  nfcsbd  2883  csbie2g  2896  csbnestgf  2898  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  csbprc  3262  csbexga  3885  bdccsb  9980