Definition df-csb 2956

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 2862, to prevent ambiguity. Theorem sbcel1g 2972 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2981 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 2955	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1298	. . . . 5 class y
7	6, 3	wcel 1448	. . . 4 wff y e. B
8	7, 1, 2	wsbc 2862	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2086	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1299	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  2957  csbeq1  2958  cbvcsb  2959  csbid  2962  csbco  2964  csbtt  2965  sbcel12g  2968  sbceqg  2969  csbeq2d  2977  csbvarg  2980  nfcsb1d  2983  nfcsbd  2986  csbie2g  3000  csbnestgf  3002  cbvralcsf  3012  cbvrexcsf  3013  cbvreucsf  3014  cbvrabcsf  3015  csbprc  3355  csbexga  3996  bdccsb  12639