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

Definition df-csb 2920
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 2826, to prevent ambiguity. Theorem sbcel1g 2936 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2945 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 2919 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1284 . . . . 5  class  y
76, 3wcel 1434 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2826 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2069 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1285 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  2921  csbeq1  2922  cbvcsb  2923  csbid  2926  csbco  2928  csbtt  2929  sbcel12g  2932  sbceqg  2933  csbeq2d  2941  csbvarg  2944  nfcsb1d  2947  nfcsbd  2950  csbie2g  2963  csbnestgf  2965  cbvralcsf  2975  cbvrexcsf  2976  cbvreucsf  2977  cbvrabcsf  2978  csbprc  3310  csbexga  3932  bdccsb  11094
  Copyright terms: Public domain W3C validator