Definition df-csb 3103

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 3006, to prevent ambiguity. Theorem sbcel1g 3121 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3131 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 3102	. 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 3006	. . 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  3104  csbeq1  3105  cbvcsbw  3106  cbvcsb  3107  csbid  3110  csbco  3112  csbcow  3113  csbtt  3114  sbcel12g  3117  sbceqg  3118  csbeq2  3126  csbeq2d  3127  csbvarg  3130  nfcsb1d  3133  nfcsbd  3138  nfcsbw  3139  csbie2g  3153  csbnestgf  3155  cbvralcsf  3165  cbvrexcsf  3166  cbvreucsf  3167  cbvrabcsf  3168  csbprc  3515  csbexga  4189  bdccsb  16103