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

Definition df-csb 3441
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 3336, to prevent ambiguity. Theorem sbcel1g 3834 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3854 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 3440 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1378 . . . . 5  class  y
76, 3wcel 1767 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3336 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2452 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1379 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3442  csbeq1  3443  csbeq2  3444  cbvcsb  3445  csbid  3448  csbco  3450  csbtt  3451  nfcsb1d  3454  nfcsbd  3457  csbie2g  3471  cbvralcsf  3472  cbvreucsf  3474  cbvrabcsf  3475  csbprc  3826  sbcel12  3828  sbcel12gOLD  3829  sbceqg  3830  csbeq2d  3839  csbnestgf  3845  csbvarg  3853  csbexg  4585  csbexgOLD  4587  csbcom2fi  30462  csbgfi  30463  bj-csbsnlem  33952  bj-csbprc  33958
  Copyright terms: Public domain W3C validator