HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef Expression
1 vx . . 3 set x
2 cA . . 3 class A
3 cB . . 3 class B
41, 2, 3csb 2805 . 2 class [_A / x]_B
5 vy . . . . . 6 set y
65cv 1614 . . . . 5 class y
76, 3wcel 1617 . . . 4 wff y e. B
87, 1, 2wsbc 1843 . . 3 wff [A / x]y e. B
98, 5cab 2157 . 2 class {y | [A / x]y e. B}
104, 9wceq 1615 1 wff [_A / x]_B = {y | [A / x]y e. B}
Colors of variables: wff set class
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