Definition df-csb 3376

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 3279, to prevent ambiguity. Theorem sbcel1g 3788 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3805 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 3375	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1454	. . . . 5 class y
7	6, 3	wcel 1898	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3279	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2448	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1455	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3377  csbeq1  3378  csbeq2  3379  cbvcsb  3380  csbid  3383  csbco  3385  csbtt  3386  nfcsb1d  3389  nfcsbd  3392  csbie2g  3406  cbvralcsf  3407  cbvreucsf  3409  cbvrabcsf  3410  csbprc  3782  sbcel12  3784  sbceqg  3785  csbeq2d  3792  csbnestgf  3797  csbvarg  3804  csbexg  4551  bj-csbsnlem  31550  bj-csbprc  31556  csbcom2fi  32414  csbgfi  32415  sbcel12gOLD  36949