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

Definition df-csb 2956
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 2862, to prevent ambiguity. Theorem sbcel1g 2972 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2981 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 2955 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1298 . . . . 5  class  y
76, 3wcel 1448 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2862 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2086 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1299 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  2957  csbeq1  2958  cbvcsb  2959  csbid  2962  csbco  2964  csbtt  2965  sbcel12g  2968  sbceqg  2969  csbeq2d  2977  csbvarg  2980  nfcsb1d  2983  nfcsbd  2986  csbie2g  3000  csbnestgf  3002  cbvralcsf  3012  cbvrexcsf  3013  cbvreucsf  3014  cbvrabcsf  3015  csbprc  3355  csbexga  3996  bdccsb  12639
  Copyright terms: Public domain W3C validator