Definition df-csb 3059

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 2963, to prevent ambiguity. Theorem sbcel1g 3077 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3087 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 3058	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1352	. . . . 5 class y
7	6, 3	wcel 2148	. . . 4 wff y e. B
8	7, 1, 2	wsbc 2963	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2163	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1353	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3060  csbeq1  3061  cbvcsbw  3062  cbvcsb  3063  csbid  3066  csbco  3068  csbcow  3069  csbtt  3070  sbcel12g  3073  sbceqg  3074  csbeq2  3082  csbeq2d  3083  csbvarg  3086  nfcsb1d  3089  nfcsbd  3093  nfcsbw  3094  csbie2g  3108  csbnestgf  3110  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  csbprc  3469  csbexga  4132  bdccsb  14615