Definition df-csb 3402

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 3305, to prevent ambiguity. Theorem sbcel1g 3812 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3829 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 3401	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1437	. . . . 5 class y
7	6, 3	wcel 1873	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3305	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2408	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1438	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  3403  csbeq1  3404  csbeq2  3405  cbvcsb  3406  csbid  3409  csbco  3411  csbtt  3412  nfcsb1d  3415  nfcsbd  3418  csbie2g  3432  cbvralcsf  3433  cbvreucsf  3435  cbvrabcsf  3436  csbprc  3806  sbcel12  3808  sbceqg  3809  csbeq2d  3816  csbnestgf  3821  csbvarg  3828  csbexg  4564  bj-csbsnlem  31480  bj-csbprc  31486  csbcom2fi  32339  csbgfi  32340  sbcel12gOLD  36881