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

Definition df-csb 3082
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 2991, to prevent ambiguity. Theorem sbcel1g 3100 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3109 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  set  x
2 cA . . 3  class  A
3 cB . . 3  class  B
41, 2, 3csb 3081 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  set  y
65cv 1622 . . . . 5  class  y
76, 3wcel 1684 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2991 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2269 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1623 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  3083  csbeq1  3084  cbvcsb  3085  csbid  3088  csbco  3090  csbexg  3091  csbtt  3093  sbcel12g  3096  sbceqg  3097  csbeq2d  3105  csbvarg  3108  nfcsb1d  3111  nfcsbd  3114  csbie2g  3127  csbnestgf  3129  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146
  Copyright terms: Public domain W3C validator