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

Definition df-csb 3254
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 3163, to prevent ambiguity. Theorem sbcel1g 3272 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3281 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 3253 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  set  y
65cv 1652 . . . . 5  class  y
76, 3wcel 1726 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3163 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2424 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1653 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  3255  csbeq1  3256  cbvcsb  3257  csbid  3260  csbco  3262  csbexg  3263  csbtt  3265  sbcel12g  3268  sbceqg  3269  csbeq2d  3277  csbvarg  3280  nfcsb1d  3283  nfcsbd  3286  csbie2g  3299  csbnestgf  3301  cbvralcsf  3313  cbvreucsf  3315  cbvrabcsf  3316
  Copyright terms: Public domain W3C validator