Definition df-csb 3138

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 3047, to prevent ambiguity. Theorem sbcel1g 3156 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3165 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 3137	. 2 class [A / x]B
5		vy	. . . . . 6 setvar y
6	5	cv 1641	. . . . 5 class y
7	6, 3	wcel 1710	. . . 4 wff y ∈ B
8	7, 1, 2	wsbc 3047	. . 3 wff [̣A / x]̣y ∈ B
9	8, 5	cab 2339	. 2 class {y ∣ [̣A / x]̣y ∈ B}
10	4, 9	wceq 1642	1 wff [A / x]B = {y ∣ [̣A / x]̣y ∈ B}

This definition is referenced by:  csb2  3139  csbeq1  3140  cbvcsb  3141  csbid  3144  csbco  3146  csbexg  3147  csbtt  3149  sbcel12g  3152  sbceqg  3153  csbeq2d  3161  csbvarg  3164  nfcsb1d  3167  nfcsbd  3170  csbie2g  3183  csbnestgf  3185  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202