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 3891
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 3775, to prevent ambiguity. Theorem sbcel1g 4409 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 4402). Theorem sbccsb 4429 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 3890 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1533 . . . . 5 class 𝑦
76, 3wcel 2099 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3775 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2705 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1534 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3892  csbeq1  3893  csbeq2  3895  csbeq2d  3896  cbvcsbw  3900  cbvcsb  3901  csbid  3903  csbcow  3905  csbco  3906  csbtt  3907  csbconstg  3909  csbgfi  3911  nfcsb1d  3913  nfcsbd  3916  nfcsbw  3917  csbie  3926  csbied  3928  csbie2g  3933  cbvralcsf  3935  cbvreucsf  3937  cbvrabcsf  3938  csbprc  4402  sbcel12  4404  sbceqg  4405  csbnestgfw  4415  csbnestgf  4420  csbvarg  4427  csbexg  5304  bj-csbsnlem  36375  bj-csbprc  36382  csbcom2fi  37595
  Copyright terms: Public domain W3C validator