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

Definition df-csb 3095
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 3004, to prevent ambiguity. Theorem sbcel1g 3113 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3122 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 3094 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  set  y
65cv 1631 . . . . 5  class  y
76, 3wcel 1696 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3004 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2282 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1632 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  3096  csbeq1  3097  cbvcsb  3098  csbid  3101  csbco  3103  csbexg  3104  csbtt  3106  sbcel12g  3109  sbceqg  3110  csbeq2d  3118  csbvarg  3121  nfcsb1d  3124  nfcsbd  3127  csbie2g  3140  csbnestgf  3142  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159
  Copyright terms: Public domain W3C validator