Definition df-csb 3141

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 3044, to prevent ambiguity. Theorem sbcel1g 3159 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3169 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 3140	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1397	. . . . 5 class y
7	6, 3	wcel 2205	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3044	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2220	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1398	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3142  csbeq1  3143  cbvcsbw  3144  cbvcsb  3145  csbid  3148  csbco  3150  csbcow  3151  csbtt  3152  sbcel12g  3155  sbceqg  3156  csbeq2  3164  csbeq2d  3165  csbvarg  3168  nfcsb1d  3171  nfcsbd  3176  nfcsbw  3177  csbie2g  3191  csbnestgf  3193  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  cbvrabcsf  3206  csbprc  3556  csbexga  4240  bdccsb  16647