Definition df-csb 3102

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 3005, to prevent ambiguity. Theorem sbcel1g 3120 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3130 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 3101	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1372	. . . . 5 class y
7	6, 3	wcel 2178	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3005	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2193	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1373	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3103  csbeq1  3104  cbvcsbw  3105  cbvcsb  3106  csbid  3109  csbco  3111  csbcow  3112  csbtt  3113  sbcel12g  3116  sbceqg  3117  csbeq2  3125  csbeq2d  3126  csbvarg  3129  nfcsb1d  3132  nfcsbd  3137  nfcsbw  3138  csbie2g  3152  csbnestgf  3154  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  csbprc  3514  csbexga  4188  bdccsb  15995