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

Definition df-csb 3252
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 3161, to prevent ambiguity. Theorem sbcel1g 3270 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3279 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 3251 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  set  y
65cv 1651 . . . . 5  class  y
76, 3wcel 1725 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3161 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2422 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1652 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  3253  csbeq1  3254  cbvcsb  3255  csbid  3258  csbco  3260  csbexg  3261  csbtt  3263  sbcel12g  3266  sbceqg  3267  csbeq2d  3275  csbvarg  3278  nfcsb1d  3281  nfcsbd  3284  csbie2g  3297  csbnestgf  3299  cbvralcsf  3311  cbvreucsf  3313  cbvrabcsf  3314
  Copyright terms: Public domain W3C validator