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 3780
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 3674, to prevent ambiguity. Theorem sbcel1g 4245 shows an example of how ambiguity could arise if we did not use distinguished brackets. When 𝐴 is a proper class, this evaluates to the empty set (see csbprc 4238). Theorem sbccsb 4263 recovers 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 3779 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1507 . . . . 5 class 𝑦
76, 3wcel 2051 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3674 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2751 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1508 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3781  csbeq1  3782  csbeq2  3783  cbvcsb  3784  csbid  3787  csbco  3789  csbtt  3790  csbgfi  3793  nfcsb1d  3795  nfcsbd  3798  csbie2g  3812  cbvralcsf  3813  cbvreucsf  3815  cbvrabcsf  3816  csbprc  4238  sbcel12  4240  sbceqg  4241  csbeq2d  4249  csbnestgf  4254  csbvarg  4261  csbexg  5067  bj-csbsnlem  33749  bj-csbprc  33755  csbcom2fi  34887
  Copyright terms: Public domain W3C validator