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

Definition df-csb 3402
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 3305, to prevent ambiguity. Theorem sbcel1g 3810 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3827 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  setvar  x
2 cA . . 3  class  A
3 cB . . 3  class  B
41, 2, 3csb 3401 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1436 . . . . 5  class  y
76, 3wcel 1870 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3305 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2414 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1437 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3403  csbeq1  3404  csbeq2  3405  cbvcsb  3406  csbid  3409  csbco  3411  csbtt  3412  nfcsb1d  3415  nfcsbd  3418  csbie2g  3432  cbvralcsf  3433  cbvreucsf  3435  cbvrabcsf  3436  csbprc  3804  sbcel12  3806  sbceqg  3807  csbeq2d  3814  csbnestgf  3819  csbvarg  3826  csbexg  4559  bj-csbsnlem  31255  bj-csbprc  31261  csbcom2fi  32076  csbgfi  32077  sbcel12gOLD  36545
  Copyright terms: Public domain W3C validator