Definition df-csb 3441

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 3336, to prevent ambiguity. Theorem sbcel1g 3834 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3854 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 3440	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1378	. . . . 5 class y
7	6, 3	wcel 1767	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3336	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2452	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1379	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3442  csbeq1  3443  csbeq2  3444  cbvcsb  3445  csbid  3448  csbco  3450  csbtt  3451  nfcsb1d  3454  nfcsbd  3457  csbie2g  3471  cbvralcsf  3472  cbvreucsf  3474  cbvrabcsf  3475  csbprc  3826  sbcel12  3828  sbcel12gOLD  3829  sbceqg  3830  csbeq2d  3839  csbnestgf  3845  csbvarg  3853  csbexg  4585  csbexgOLD  4587  csbcom2fi  30462  csbgfi  30463  bj-csbsnlem  33952  bj-csbprc  33958