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 3729
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 3633, to prevent ambiguity. Theorem sbcel1g 4184 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 4178). Theorem sbccsb 4202 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 3728 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1636 . . . . 5 class 𝑦
76, 3wcel 2156 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3633 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2792 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1637 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3730  csbeq1  3731  csbeq2  3732  cbvcsb  3733  csbid  3736  csbco  3738  csbtt  3739  nfcsb1d  3742  nfcsbd  3745  csbie2g  3759  cbvralcsf  3760  cbvreucsf  3762  cbvrabcsf  3763  csbprc  4178  sbcel12  4180  sbceqg  4181  csbeq2d  4188  csbnestgf  4193  csbvarg  4200  csbexg  4987  bj-csbsnlem  33201  bj-csbprc  33207  csbcom2fi  34239  csbgfi  34240  sbcel12gOLD  39246
  Copyright terms: Public domain W3C validator