Definition df-csb 3137

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 3046, to prevent ambiguity. Theorem sbcel1g 3155 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3164 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 3136	. 2 class [_A / x]_B
5		vy	. . . . . 6 setvar y
6	5	cv 1641	. . . . 5 class y
7	6, 3	wcel 1710	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3046	. . 3 wff [.A / x ].y e. B
9	8, 5	cab 2339	. 2 class {y | [.A / x ].y e. B}
10	4, 9	wceq 1642	1 wff [_A / x]_B = {y | [.A / x ].y e. B}

This definition is referenced by:  csb2  3138  csbeq1  3139  cbvcsb  3140  csbid  3143  csbco  3145  csbexg  3146  csbtt  3148  sbcel12g  3151  sbceqg  3152  csbeq2d  3160  csbvarg  3163  nfcsb1d  3166  nfcsbd  3169  csbie2g  3182  csbnestgf  3184  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201