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

Definition df-csb 2850
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 2761, to prevent ambiguity. Theorem sbcel1g 2866 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2875 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 2849 . 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 2761 . . 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  2851  csbeq1  2852  cbvcsb  2853  csbid  2856  csbco  2858  csbtt  2859  sbcel12g  2862  sbceqg  2863  csbeq2d  2871  csbvarg  2874  nfcsb1d  2877  nfcsbd  2880  csbie2g  2893  csbnestgf  2895  cbvralcsf  2905  cbvrexcsf  2906  cbvreucsf  2907  cbvrabcsf  2908  csbprc  3259  csbexga  3882  bdccsb  9844
  Copyright terms: Public domain W3C validator