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

Definition df-csb 2880
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 2786, to prevent ambiguity. Theorem sbcel1g 2896 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2905 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 2879 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1258 . . . . 5  class  y
76, 3wcel 1409 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2786 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2042 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1259 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  2881  csbeq1  2882  cbvcsb  2883  csbid  2886  csbco  2888  csbtt  2889  sbcel12g  2892  sbceqg  2893  csbeq2d  2901  csbvarg  2904  nfcsb1d  2907  nfcsbd  2910  csbie2g  2923  csbnestgf  2925  cbvralcsf  2935  cbvrexcsf  2936  cbvreucsf  2937  cbvrabcsf  2938  csbprc  3289  csbexga  3912  bdccsb  10346
  Copyright terms: Public domain W3C validator