Definition df-csb 3056

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 2960, to prevent ambiguity. Theorem sbcel1g 3074 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3084 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 3055	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1352	. . . . 5 class y
7	6, 3	wcel 2146	. . . 4 wff y e. B
8	7, 1, 2	wsbc 2960	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2161	. 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  3057  csbeq1  3058  cbvcsbw  3059  cbvcsb  3060  csbid  3063  csbco  3065  csbcow  3066  csbtt  3067  sbcel12g  3070  sbceqg  3071  csbeq2  3079  csbeq2d  3080  csbvarg  3083  nfcsb1d  3086  nfcsbd  3090  nfcsbw  3091  csbie2g  3105  csbnestgf  3107  cbvralcsf  3117  cbvrexcsf  3118  cbvreucsf  3119  cbvrabcsf  3120  csbprc  3466  csbexga  4126  bdccsb  14181