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 3900
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 3788, to prevent ambiguity. Theorem sbcel1g 4416 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 4409). Theorem sbccsb 4436 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 3899 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1539 . . . . 5 class 𝑦
76, 3wcel 2108 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3788 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2714 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1540 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3901  csbeq1  3902  csbeq2  3904  csbeq2d  3905  csbeq2dv  3906  cbvcsbw  3909  cbvcsb  3910  cbvcsbv  3911  csbid  3912  csbcow  3914  csbco  3915  csbtt  3916  csbconstg  3918  csbgfi  3919  nfcsb1d  3921  nfcsbd  3924  nfcsbw  3925  csbie  3934  csbied  3935  csbie2g  3939  cbvralcsf  3941  cbvreucsf  3943  cbvrabcsf  3944  csbprc  4409  sbcel12  4411  sbceqg  4412  csbnestgfw  4422  csbnestgf  4427  csbvarg  4434  csbexg  5310  cbvcsbvw2  36232  cbvcsbdavw  36260  cbvcsbdavw2  36261  bj-csbsnlem  36904  bj-csbprc  36911  csbcom2fi  38135
  Copyright terms: Public domain W3C validator