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

Definition df-csb 3004
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 2909, to prevent ambiguity. Theorem sbcel1g 3021 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3031 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 3003 . 2  class  [_ A  /  x ]_ B
5 vy . . . . . 6  setvar  y
65cv 1330 . . . . 5  class  y
76, 3wcel 1480 . . . 4  wff  y  e.  B
87, 1, 2wsbc 2909 . . 3  wff  [. A  /  x ]. y  e.  B
98, 5cab 2125 . 2  class  { y  |  [. A  /  x ]. y  e.  B }
104, 9wceq 1331 1  wff  [_ A  /  x ]_ B  =  { y  |  [. A  /  x ]. y  e.  B }
Colors of variables: wff set class
This definition is referenced by:  csb2  3005  csbeq1  3006  cbvcsbw  3007  cbvcsb  3008  csbid  3011  csbco  3013  csbtt  3014  sbcel12g  3017  sbceqg  3018  csbeq2  3026  csbeq2d  3027  csbvarg  3030  nfcsb1d  3033  nfcsbd  3036  csbie2g  3050  csbnestgf  3052  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  csbprc  3408  csbexga  4056  bdccsb  13142
  Copyright terms: Public domain W3C validator