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 3499
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 3401, to prevent ambiguity. Theorem sbcel1g 3938 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3955 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 3498 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1473 . . . . 5 class 𝑦
76, 3wcel 1976 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3401 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2595 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1474 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3500  csbeq1  3501  csbeq2  3502  cbvcsb  3503  csbid  3506  csbco  3508  csbtt  3509  nfcsb1d  3512  nfcsbd  3515  csbie2g  3529  cbvralcsf  3530  cbvreucsf  3532  cbvrabcsf  3533  csbprc  3931  csbprcOLD  3932  sbcel12  3934  sbceqg  3935  csbeq2d  3942  csbnestgf  3947  csbvarg  3954  csbexg  4714  bj-csbsnlem  31873  bj-csbprc  31879  csbcom2fi  32887  csbgfi  32888  sbcel12gOLD  37558
  Copyright terms: Public domain W3C validator