Definition df-csb 3421

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 3324, to prevent ambiguity. Theorem sbcel1g 3826 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3843 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 3420	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1397	. . . . 5 class y
7	6, 3	wcel 1823	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3324	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2439	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1398	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3422  csbeq1  3423  csbeq2  3424  cbvcsb  3425  csbid  3428  csbco  3430  csbtt  3431  nfcsb1d  3434  nfcsbd  3437  csbie2g  3451  cbvralcsf  3452  cbvreucsf  3454  cbvrabcsf  3455  csbprc  3820  sbcel12  3822  sbceqg  3823  csbeq2d  3830  csbnestgf  3835  csbvarg  3842  csbexg  4571  csbcom2fi  30777  csbgfi  30778  sbcel12gOLD  33724  bj-csbsnlem  34890  bj-csbprc  34896