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 3313, to prevent ambiguity. Theorem sbcel1g 3815 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3835 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 1382	. . . . 5 class y
7	6, 3	wcel 1804	. . . 4 wff y e. B
8	7, 1, 2	wsbc 3313	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2428	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1383	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  3807  sbcel12  3809  sbcel12gOLD  3810  sbceqg  3811  csbeq2d  3820  csbnestgf  3826  csbvarg  3834  csbexg  4569  csbexgOLD  4571  csbcom2fi  30510  csbgfi  30511  bj-csbsnlem  34353  bj-csbprc  34359