Definition df-csb 2821

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 2732, to prevent ambiguity. Theorem sbcel1g 2837 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2846 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 ∈ 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 2820	. 2 class ⦋A / x⦌B
5		vy	. . . . . 6 setvar y
6	5	cv 1222	. . . . 5 class y
7	6, 3	wcel 1366	. . . 4 wff y ∈ B
8	7, 1, 2	wsbc 2732	. . 3 wff [A / x]y ∈ B
9	8, 5	cab 1999	. 2 class {y ∣ [A / x]y ∈ B}
10	4, 9	wceq 1223	1 wff ⦋A / x⦌B = {y ∣ [A / x]y ∈ B}

This definition is referenced by:  csb2  2822  csbeq1  2823  cbvcsb  2824  csbid  2827  csbco  2829  csbtt  2830  sbcel12g  2833  sbceqg  2834  csbeq2d  2842  csbvarg  2845  nfcsb1d  2848  nfcsbd  2851  csbie2g  2864  csbnestgf  2866  cbvralcsf  2876  cbvrexcsf  2877  cbvreucsf  2878  cbvrabcsf  2879  csbprc  3230  csbexga  3848  bdccsb  8245