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

Definition df-csb 2853
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 2764, to prevent ambiguity. Theorem sbcel1g 2869 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2878 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 2852 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1242 . . . . 5  class  y
76, 3wcel 1393 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2764 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2026 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1243 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  2854  csbeq1  2855  cbvcsb  2856  csbid  2859  csbco  2861  csbtt  2862  sbcel12g  2865  sbceqg  2866  csbeq2d  2874  csbvarg  2877  nfcsb1d  2880  nfcsbd  2883  csbie2g  2896  csbnestgf  2898  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  csbprc  3262  csbexga  3885  bdccsb  9980
  Copyright terms: Public domain W3C validator