Definition df-csb 3094

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 2998, to prevent ambiguity. Theorem sbcel1g 3112 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3122 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 3093	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1372	. . . . 5 class y
7	6, 3	wcel 2176	. . . 4 wff y e. B
8	7, 1, 2	wsbc 2998	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2191	. 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  3095  csbeq1  3096  cbvcsbw  3097  cbvcsb  3098  csbid  3101  csbco  3103  csbcow  3104  csbtt  3105  sbcel12g  3108  sbceqg  3109  csbeq2  3117  csbeq2d  3118  csbvarg  3121  nfcsb1d  3124  nfcsbd  3129  nfcsbw  3130  csbie2g  3144  csbnestgf  3146  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  csbprc  3506  csbexga  4172  bdccsb  15796