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 3812 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3829 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 1437 . . . . 5  class  y
76, 3wcel 1873 . . . 4  wff  y  e.  B
87, 1, 2wsbc 3305 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2408 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1438 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  3806  sbcel12  3808  sbceqg  3809  csbeq2d  3816  csbnestgf  3821  csbvarg  3828  csbexg  4564  bj-csbsnlem  31480  bj-csbprc  31486  csbcom2fi  32339  csbgfi  32340  sbcel12gOLD  36881
  Copyright terms: Public domain W3C validator