Definition df-csb 2826

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 2737, to prevent ambiguity. Theorem sbcel1g 2842 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2851 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 2825	. 2 class ⦋A / x⦌B
5		vy	. . . . . 6 setvar y
6	5	cv 1225	. . . . 5 class y
7	6, 3	wcel 1370	. . . 4 wff y ∈ B
8	7, 1, 2	wsbc 2737	. . 3 wff [A / x]y ∈ B
9	8, 5	cab 2004	. 2 class {y ∣ [A / x]y ∈ B}
10	4, 9	wceq 1226	1 wff ⦋A / x⦌B = {y ∣ [A / x]y ∈ B}

This definition is referenced by:  csb2  2827  csbeq1  2828  cbvcsb  2829  csbid  2832  csbco  2834  csbtt  2835  sbcel12g  2838  sbceqg  2839  csbeq2d  2847  csbvarg  2850  nfcsb1d  2853  nfcsbd  2856  csbie2g  2869  csbnestgf  2871  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  cbvrabcsf  2884  csbprc  3235  csbexgOLD  3855  bdccsb  7226