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 3883
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 3771, to prevent ambiguity. Theorem sbcel1g 4364 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 4357). Theorem sbccsb 4384 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 3882 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1527 . . . . 5 class 𝑦
76, 3wcel 2105 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3771 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2799 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1528 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3884  csbeq1  3885  csbeq2  3887  csbeq2d  3888  cbvcsbw  3892  cbvcsb  3893  csbid  3895  csbcow  3897  csbco  3898  csbtt  3899  csbgfi  3902  nfcsb1d  3904  nfcsbd  3907  nfcsbw  3908  csbie2g  3922  cbvralcsf  3924  cbvreucsf  3926  cbvrabcsf  3927  csbprc  4357  sbcel12  4359  sbceqg  4360  csbnestgfw  4370  csbnestgf  4375  csbvarg  4382  csbexg  5206  bj-csbsnlem  34118  bj-csbprc  34124  csbcom2fi  35289
  Copyright terms: Public domain W3C validator