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 3567
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 3468, to prevent ambiguity. Theorem sbcel1g 4020 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 4037 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 3566 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1522 . . . . 5 class 𝑦
76, 3wcel 2030 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3468 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2637 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1523 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3568  csbeq1  3569  csbeq2  3570  cbvcsb  3571  csbid  3574  csbco  3576  csbtt  3577  nfcsb1d  3580  nfcsbd  3583  csbie2g  3597  cbvralcsf  3598  cbvreucsf  3600  cbvrabcsf  3601  csbprc  4013  csbprcOLD  4014  sbcel12  4016  sbceqg  4017  csbeq2d  4024  csbnestgf  4029  csbvarg  4036  csbexg  4825  bj-csbsnlem  33023  bj-csbprc  33029  csbcom2fi  34064  csbgfi  34065  sbcel12gOLD  39071
  Copyright terms: Public domain W3C validator