Definition df-csb 3402

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 3305, to prevent ambiguity. Theorem sbcel1g 3810 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3827 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
df-csb	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }

Distinct variable groups:   y, A   y, B   x, y

Allowed substitution hints:   A( x)   B( x)

Detailed syntax breakdown of Definition df-csb

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar x
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	csb 3401	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1436	. . . . 5 class y
7	6, 3	wcel 1870	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3305	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2414	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1437	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3403  csbeq1  3404  csbeq2  3405  cbvcsb  3406  csbid  3409  csbco  3411  csbtt  3412  nfcsb1d  3415  nfcsbd  3418  csbie2g  3432  cbvralcsf  3433  cbvreucsf  3435  cbvrabcsf  3436  csbprc  3804  sbcel12  3806  sbceqg  3807  csbeq2d  3814  csbnestgf  3819  csbvarg  3826  csbexg  4559  bj-csbsnlem  31255  bj-csbprc  31261  csbcom2fi  32076  csbgfi  32077  sbcel12gOLD  36545