Definition df-csb 2847

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

This definition is referenced by:  csb2  2848  csbeq1  2849  cbvcsb  2850  csbid  2853  csbco  2855  csbtt  2856  sbcel12g  2859  sbceqg  2860  csbeq2d  2868  csbvarg  2871  nfcsb1d  2874  nfcsbd  2877  csbie2g  2890  csbnestgf  2892  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  csbprc  3256  csbexga  3876  bdccsb  9295