Definition df-csb 3081

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 2985, to prevent ambiguity. Theorem sbcel1g 3099 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3109 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 3080	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1363	. . . . 5 class y
7	6, 3	wcel 2164	. . . 4 wff y e. B
8	7, 1, 2	wsbc 2985	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2179	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1364	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3082  csbeq1  3083  cbvcsbw  3084  cbvcsb  3085  csbid  3088  csbco  3090  csbcow  3091  csbtt  3092  sbcel12g  3095  sbceqg  3096  csbeq2  3104  csbeq2d  3105  csbvarg  3108  nfcsb1d  3111  nfcsbd  3116  nfcsbw  3117  csbie2g  3131  csbnestgf  3133  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  csbprc  3492  csbexga  4157  bdccsb  15352