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

Definition df-csb 3421
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 3313, to prevent ambiguity. Theorem sbcel1g 3815 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3835 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 3420 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1382 . . . . 5  class  y
76, 3wcel 1804 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3313 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2428 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1383 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3422  csbeq1  3423  csbeq2  3424  cbvcsb  3425  csbid  3428  csbco  3430  csbtt  3431  nfcsb1d  3434  nfcsbd  3437  csbie2g  3451  cbvralcsf  3452  cbvreucsf  3454  cbvrabcsf  3455  csbprc  3807  sbcel12  3809  sbcel12gOLD  3810  sbceqg  3811  csbeq2d  3820  csbnestgf  3826  csbvarg  3834  csbexg  4569  csbexgOLD  4571  csbcom2fi  30510  csbgfi  30511  bj-csbsnlem  34353  bj-csbprc  34359
  Copyright terms: Public domain W3C validator