Definition df-csb 3073

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 2977, to prevent ambiguity. Theorem sbcel1g 3091 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3101 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 3072	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1363	. . . . 5 class y
7	6, 3	wcel 2160	. . . 4 wff y e. B
8	7, 1, 2	wsbc 2977	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2175	. 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  3074  csbeq1  3075  cbvcsbw  3076  cbvcsb  3077  csbid  3080  csbco  3082  csbcow  3083  csbtt  3084  sbcel12g  3087  sbceqg  3088  csbeq2  3096  csbeq2d  3097  csbvarg  3100  nfcsb1d  3103  nfcsbd  3107  nfcsbw  3108  csbie2g  3122  csbnestgf  3124  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  csbprc  3483  csbexga  4146  bdccsb  15049