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

Definition df-csb 3073
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 2977, to prevent ambiguity. Theorem sbcel1g 3091 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3101 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 3072 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1363 . . . . 5  class  y
76, 3wcel 2160 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2977 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2175 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1364 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  3074  csbeq1  3075  cbvcsbw  3076  cbvcsb  3077  csbid  3080  csbco  3082  csbcow  3083  csbtt  3084  sbcel12g  3087  sbceqg  3088  csbeq2  3096  csbeq2d  3097  csbvarg  3100  nfcsb1d  3103  nfcsbd  3107  nfcsbw  3108  csbie2g  3122  csbnestgf  3124  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  cbvrabcsf  3137  csbprc  3483  csbexga  4146  bdccsb  15049
  Copyright terms: Public domain W3C validator