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

Definition df-csb 3376
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 3279, to prevent ambiguity. Theorem sbcel1g 3788 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3805 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 3375 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1454 . . . . 5  class  y
76, 3wcel 1898 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3279 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2448 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1455 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3377  csbeq1  3378  csbeq2  3379  cbvcsb  3380  csbid  3383  csbco  3385  csbtt  3386  nfcsb1d  3389  nfcsbd  3392  csbie2g  3406  cbvralcsf  3407  cbvreucsf  3409  cbvrabcsf  3410  csbprc  3782  sbcel12  3784  sbceqg  3785  csbeq2d  3792  csbnestgf  3797  csbvarg  3804  csbexg  4551  bj-csbsnlem  31550  bj-csbprc  31556  csbcom2fi  32414  csbgfi  32415  sbcel12gOLD  36949
  Copyright terms: Public domain W3C validator