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

Definition df-csb 2974
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 2880, to prevent ambiguity. Theorem sbcel1g 2990 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2999 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
df-csb 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-csb
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3csb 2973 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1313 . . . . 5 class 𝑦
76, 3wcel 1463 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 2880 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2101 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1314 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff set class
This definition is referenced by:  csb2  2975  csbeq1  2976  cbvcsb  2977  csbid  2980  csbco  2982  csbtt  2983  sbcel12g  2986  sbceqg  2987  csbeq2d  2995  csbvarg  2998  nfcsb1d  3001  nfcsbd  3004  csbie2g  3018  csbnestgf  3020  cbvralcsf  3030  cbvrexcsf  3031  cbvreucsf  3032  cbvrabcsf  3033  csbprc  3376  csbexga  4024  bdccsb  12892
  Copyright terms: Public domain W3C validator