Definition df-csb 2541

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 1534, to prevent ambiguity. Theorem sbcel1g 2556 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2565 recreates substitution into a wff from this definition.

Assertion

Ref	Expression
df-csb	|- [_A / x]_B = {y | [A / x]y e. B}

Distinct variable groups:   y,A   y,B   x,y

Detailed syntax breakdown of Definition df-csb

Step	Hyp	Ref	Expression
1		vx	. . 3 set x
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	csb 2540	. 2 class [_A / x]_B
5		vy	. . . . . 6 set y
6	5	cv 1297	. . . . 5 class y
7	6, 3	wcel 1300	. . . 4 wff y e. B
8	7, 1, 2	wsbc 1534	. . 3 wff [A / x]y e. B
9	8, 5	cab 1871	. 2 class {y | [A / x]y e. B}
10	4, 9	wceq 1298	1 wff [_A / x]_B = {y | [A / x]y e. B}

This definition is referenced by:  csbeq1 2542  cbvcsbv 2543  csbid 2545  csbcog 2547  csbexg 2548  csbconstgf 2551  sbcel12g 2552  sbcel12gOLD 2553  sbceqdig 2554  sbceqdigOLD 2555  csbvarg 2564  hbcsb1g 2567  hbcsbg 2569  csbiegft 2573  csbabgOLD 2589  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414

Copyright terms: Public domain