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

Definition df-csb 2821
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 2732, to prevent ambiguity. Theorem sbcel1g 2837 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2846 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
df-csb A / xB = {y[A / x]y 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 2820 . 2 class A / xB
5 vy . . . . . 6 setvar y
65cv 1222 . . . . 5 class y
76, 3wcel 1366 . . . 4 wff y B
87, 1, 2wsbc 2732 . . 3 wff [A / x]y B
98, 5cab 1999 . 2 class {y[A / x]y B}
104, 9wceq 1223 1 wff A / xB = {y[A / x]y B}
Colors of variables: wff set class
This definition is referenced by:  csb2  2822  csbeq1  2823  cbvcsb  2824  csbid  2827  csbco  2829  csbtt  2830  sbcel12g  2833  sbceqg  2834  csbeq2d  2842  csbvarg  2845  nfcsb1d  2848  nfcsbd  2851  csbie2g  2864  csbnestgf  2866  cbvralcsf  2876  cbvrexcsf  2877  cbvreucsf  2878  cbvrabcsf  2879  csbprc  3230  csbexga  3848  bdccsb  8245
  Copyright terms: Public domain W3C validator