Definition df-csb 3212

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 3121, to prevent ambiguity. Theorem sbcel1g 3230 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3239 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 set x
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	csb 3211	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 set y
6	5	cv 1648	. . . . 5 class y
7	6, 3	wcel 1721	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3121	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2390	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1649	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3213  csbeq1  3214  cbvcsb  3215  csbid  3218  csbco  3220  csbexg  3221  csbtt  3223  sbcel12g  3226  sbceqg  3227  csbeq2d  3235  csbvarg  3238  nfcsb1d  3241  nfcsbd  3244  csbie2g  3257  csbnestgf  3259  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274