Definition df-csb 2806

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 1843, to prevent ambiguity. Theorem sbcel1g 2819 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2828 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 2805	. 2 class [_A / x]_B
5		vy	. . . . . 6 set y
6	5	cv 1614	. . . . 5 class y
7	6, 3	wcel 1617	. . . 4 wff y e. B
8	7, 1, 2	wsbc 1843	. . 3 wff [A / x]y e. B
9	8, 5	cab 2157	. 2 class {y | [A / x]y e. B}
10	4, 9	wceq 1615	1 wff [_A / x]_B = {y | [A / x]y e. B}

This definition is referenced by:  csbeq1 2807  cbvcsbv 2808  csbid 2810  csbcog 2812  csbexg 2813  csbconstgf 2815  sbcel12g 2817  sbceqg 2818  csbvarg 2827  hbcsb1g 2830  hbcsbg 2832  csbiegft 2836  cbvralcsf 2852  cbvrexcsf 2853  cbvreucsf 2854  cbvrabcsf 2855  cbvralcsfOLD 17496  cbvrexcsfOLD 17497  cbvreucsfOLD 17498  cbvrabcsfOLD 17499

Copyright terms: Public domain