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 3520
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 3422, to prevent ambiguity. Theorem sbcel1g 3965 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3982 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 3519 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1479 . . . . 5 class 𝑦
76, 3wcel 1987 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3422 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2607 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1480 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3521  csbeq1  3522  csbeq2  3523  cbvcsb  3524  csbid  3527  csbco  3529  csbtt  3530  nfcsb1d  3533  nfcsbd  3536  csbie2g  3550  cbvralcsf  3551  cbvreucsf  3553  cbvrabcsf  3554  csbprc  3958  csbprcOLD  3959  sbcel12  3961  sbceqg  3962  csbeq2d  3969  csbnestgf  3974  csbvarg  3981  csbexg  4762  bj-csbsnlem  32598  bj-csbprc  32604  csbcom2fi  33605  csbgfi  33606  sbcel12gOLD  38275
  Copyright terms: Public domain W3C validator