MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-csb Structured version   Visualization version   GIF version

Definition df-csb 3667
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 3568, to prevent ambiguity. Theorem sbcel1g 4122 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 4139 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 3666 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1623 . . . . 5 class 𝑦
76, 3wcel 2131 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3568 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2738 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1624 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3668  csbeq1  3669  csbeq2  3670  cbvcsb  3671  csbid  3674  csbco  3676  csbtt  3677  nfcsb1d  3680  nfcsbd  3683  csbie2g  3697  cbvralcsf  3698  cbvreucsf  3700  cbvrabcsf  3701  csbprc  4115  csbprcOLD  4116  sbcel12  4118  sbceqg  4119  csbeq2d  4126  csbnestgf  4131  csbvarg  4138  csbexg  4936  bj-csbsnlem  33196  bj-csbprc  33202  csbcom2fi  34239  csbgfi  34240  sbcel12gOLD  39248
  Copyright terms: Public domain W3C validator