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

Definition df-csb 3085
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 2994, to prevent ambiguity. Theorem sbcel1g 3103 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3112 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 groups:    A( x)    B( x)

Detailed syntax breakdown of Definition df-csb
StepHypRef Expression
1 vx . . 3  set  x
2 cA . . 3  class  A
3 cB . . 3  class  B
41, 2, 3csb 3084 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  set  y
65cv 1624 . . . . 5  class  y
76, 3wcel 1687 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2994 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2272 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1625 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  3086  csbeq1  3087  cbvcsb  3088  csbid  3091  csbco  3093  csbexg  3094  csbtt  3096  sbcel12g  3099  sbceqg  3100  csbeq2d  3108  csbvarg  3111  nfcsb1d  3114  nfcsbd  3117  csbie2g  3130  csbnestgf  3132  cbvralcsf  3146  cbvreucsf  3148  cbvrabcsf  3149
  Copyright terms: Public domain W3C validator