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 3856
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 3747, to prevent ambiguity. Theorem sbcel1g 4337 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 4330). Theorem sbccsb 4357 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 3855 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1537 . . . . 5 class 𝑦
76, 3wcel 2114 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3747 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2800 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1538 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3857  csbeq1  3858  csbeq2  3860  csbeq2d  3861  cbvcsbw  3865  cbvcsb  3866  csbid  3868  csbcow  3870  csbco  3871  csbtt  3872  csbgfi  3875  nfcsb1d  3877  nfcsbd  3880  nfcsbw  3881  csbie2g  3895  cbvralcsf  3897  cbvreucsf  3899  cbvrabcsf  3900  csbprc  4330  sbcel12  4332  sbceqg  4333  csbnestgfw  4343  csbnestgf  4348  csbvarg  4355  csbexg  5190  bj-csbsnlem  34305  bj-csbprc  34311  csbcom2fi  35528
  Copyright terms: Public domain W3C validator