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

Definition df-csb 2910
 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 2816, to prevent ambiguity. Theorem sbcel1g 2926 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2935 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 2909 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1284 . . . . 5 class 𝑦
76, 3wcel 1434 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 2816 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2068 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1285 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
 Colors of variables: wff set class This definition is referenced by:  csb2  2911  csbeq1  2912  cbvcsb  2913  csbid  2916  csbco  2918  csbtt  2919  sbcel12g  2922  sbceqg  2923  csbeq2d  2931  csbvarg  2934  nfcsb1d  2937  nfcsbd  2940  csbie2g  2953  csbnestgf  2955  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  csbprc  3290  csbexga  3908  bdccsb  10794
 Copyright terms: Public domain W3C validator