ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-csb Unicode version

Definition df-csb 2923
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 2829, to prevent ambiguity. Theorem sbcel1g 2939 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2948 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 2922 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1286 . . . . 5  class  y
76, 3wcel 1436 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2829 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2071 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1287 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  2924  csbeq1  2925  cbvcsb  2926  csbid  2929  csbco  2931  csbtt  2932  sbcel12g  2935  sbceqg  2936  csbeq2d  2944  csbvarg  2947  nfcsb1d  2950  nfcsbd  2953  csbie2g  2967  csbnestgf  2969  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  csbprc  3316  csbexga  3944  bdccsb  11220
  Copyright terms: Public domain W3C validator