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 3324, to prevent ambiguity. Theorem sbcel1g 3826 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3843 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 1397 . . . . 5  class  y
76, 3wcel 1823 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3324 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2439 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1398 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  3820  sbcel12  3822  sbceqg  3823  csbeq2d  3830  csbnestgf  3835  csbvarg  3842  csbexg  4571  csbcom2fi  30777  csbgfi  30778  sbcel12gOLD  33724  bj-csbsnlem  34890  bj-csbprc  34896
  Copyright terms: Public domain W3C validator