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

Definition df-csb 3244
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 3153, to prevent ambiguity. Theorem sbcel1g 3262 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3271 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 3243 . 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 3153 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2421 . 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  3245  csbeq1  3246  cbvcsb  3247  csbid  3250  csbco  3252  csbexg  3253  csbtt  3255  sbcel12g  3258  sbceqg  3259  csbeq2d  3267  csbvarg  3270  nfcsb1d  3273  nfcsbd  3276  csbie2g  3289  csbnestgf  3291  cbvralcsf  3303  cbvreucsf  3305  cbvrabcsf  3306
  Copyright terms: Public domain W3C validator