Definition df-csb 3085

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 2989, to prevent ambiguity. Theorem sbcel1g 3103 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3113 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 3084	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1363	. . . . 5 class y
7	6, 3	wcel 2167	. . . 4 wff y e. B
8	7, 1, 2	wsbc 2989	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2182	. 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  3086  csbeq1  3087  cbvcsbw  3088  cbvcsb  3089  csbid  3092  csbco  3094  csbcow  3095  csbtt  3096  sbcel12g  3099  sbceqg  3100  csbeq2  3108  csbeq2d  3109  csbvarg  3112  nfcsb1d  3115  nfcsbd  3120  nfcsbw  3121  csbie2g  3135  csbnestgf  3137  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  csbprc  3496  csbexga  4161  bdccsb  15506