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

Definition df-csb 2847
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 2758, to prevent ambiguity. Theorem sbcel1g 2863 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2872 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 2846 . 2 class A / xB
5 vy . . . . . 6 setvar y
65cv 1241 . . . . 5 class y
76, 3wcel 1390 . . . 4 wff y B
87, 1, 2wsbc 2758 . . 3 wff [A / x]y B
98, 5cab 2023 . 2 class {y[A / x]y B}
104, 9wceq 1242 1 wff A / xB = {y[A / x]y B}
Colors of variables: wff set class
This definition is referenced by:  csb2  2848  csbeq1  2849  cbvcsb  2850  csbid  2853  csbco  2855  csbtt  2856  sbcel12g  2859  sbceqg  2860  csbeq2d  2868  csbvarg  2871  nfcsb1d  2874  nfcsbd  2877  csbie2g  2890  csbnestgf  2892  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  csbprc  3256  csbexga  3876  bdccsb  9249
  Copyright terms: Public domain W3C validator