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

Definition df-csb 2826
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 2737, to prevent ambiguity. Theorem sbcel1g 2842 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2851 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 2825 . 2 class A / xB
5 vy . . . . . 6 setvar y
65cv 1225 . . . . 5 class y
76, 3wcel 1370 . . . 4 wff y B
87, 1, 2wsbc 2737 . . 3 wff [A / x]y B
98, 5cab 2004 . 2 class {y[A / x]y B}
104, 9wceq 1226 1 wff A / xB = {y[A / x]y B}
Colors of variables: wff set class
This definition is referenced by:  csb2  2827  csbeq1  2828  cbvcsb  2829  csbid  2832  csbco  2834  csbtt  2835  sbcel12g  2838  sbceqg  2839  csbeq2d  2847  csbvarg  2850  nfcsb1d  2853  nfcsbd  2856  csbie2g  2869  csbnestgf  2871  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  cbvrabcsf  2884  csbprc  3235  csbexgOLD  3855  bdccsb  7226
  Copyright terms: Public domain W3C validator