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

Definition df-csb 3043
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 2952, to prevent ambiguity. Theorem sbcel1g 3061 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3070 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 3042 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  set  y
65cv 1618 . . . . 5  class  y
76, 3wcel 1621 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2952 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2242 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1619 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  3044  csbeq1  3045  cbvcsb  3046  csbid  3049  csbco  3051  csbexg  3052  csbtt  3054  sbcel12g  3057  sbceqg  3058  csbeq2d  3066  csbvarg  3069  nfcsb1d  3072  nfcsbd  3075  csbie2g  3088  csbnestgf  3090  cbvralcsf  3104  cbvreucsf  3106  cbvrabcsf  3107
  Copyright terms: Public domain W3C validator