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

Definition df-csb 2976
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 2882, to prevent ambiguity. Theorem sbcel1g 2992 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3001 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 2975 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1315 . . . . 5  class  y
76, 3wcel 1465 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2882 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2103 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1316 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  2977  csbeq1  2978  cbvcsb  2979  csbid  2982  csbco  2984  csbtt  2985  sbcel12g  2988  sbceqg  2989  csbeq2d  2997  csbvarg  3000  nfcsb1d  3003  nfcsbd  3006  csbie2g  3020  csbnestgf  3022  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  csbprc  3378  csbexga  4026  bdccsb  12954
  Copyright terms: Public domain W3C validator