MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-csb Unicode version

Definition df-csb 3212
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 3121, to prevent ambiguity. Theorem sbcel1g 3230 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3239 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  e.  B }
Distinct variable groups:    y, A    y, B    x, y
Allowed substitution hints:    A( x)    B( x)

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 3211 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  set  y
65cv 1648 . . . . 5  class  y
76, 3wcel 1721 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3121 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2390 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1649 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  3213  csbeq1  3214  cbvcsb  3215  csbid  3218  csbco  3220  csbexg  3221  csbtt  3223  sbcel12g  3226  sbceqg  3227  csbeq2d  3235  csbvarg  3238  nfcsb1d  3241  nfcsbd  3244  csbie2g  3257  csbnestgf  3259  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274
  Copyright terms: Public domain W3C validator