Definition df-csb 2923

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 2829, to prevent ambiguity. Theorem sbcel1g 2939 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2948 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 2922	. 2 class [_ A / x ]_ B
5		vy	. . . . . 6 setvar y
6	5	cv 1286	. . . . 5 class y
7	6, 3	wcel 1436	. . . 4 wff y e. B
8	7, 1, 2	wsbc 2829	. . 3 wff [. A / x ]. y e. B
9	8, 5	cab 2071	. 2 class { y | [. A / x ]. y e. B }
10	4, 9	wceq 1287	1 wff [_ A / x ]_ B = { y | [. A / x ]. y e. B }

This definition is referenced by:  csb2  2924  csbeq1  2925  cbvcsb  2926  csbid  2929  csbco  2931  csbtt  2932  sbcel12g  2935  sbceqg  2936  csbeq2d  2944  csbvarg  2947  nfcsb1d  2950  nfcsbd  2953  csbie2g  2967  csbnestgf  2969  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  csbprc  3316  csbexga  3944  bdccsb  11220