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 3895
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 3778, to prevent ambiguity. Theorem sbcel1g 4414 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 4407). Theorem sbccsb 4434 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 3894 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1541 . . . . 5 class 𝑦
76, 3wcel 2107 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3778 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2710 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1542 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3896  csbeq1  3897  csbeq2  3899  csbeq2d  3900  cbvcsbw  3904  cbvcsb  3905  csbid  3907  csbcow  3909  csbco  3910  csbtt  3911  csbconstg  3913  csbgfi  3915  nfcsb1d  3917  nfcsbd  3920  nfcsbw  3921  csbie  3930  csbied  3932  csbie2g  3937  cbvralcsf  3939  cbvreucsf  3941  cbvrabcsf  3942  csbprc  4407  sbcel12  4409  sbceqg  4410  csbnestgfw  4420  csbnestgf  4425  csbvarg  4432  csbexg  5311  bj-csbsnlem  35783  bj-csbprc  35790  csbcom2fi  36996
  Copyright terms: Public domain W3C validator