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 3500
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 3402, to prevent ambiguity. Theorem sbcel1g 3939 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3956 recreates 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 3499 . 2 class 𝐴 / 𝑥𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1474 . . . . 5 class 𝑦
76, 3wcel 1977 . . . 4 wff 𝑦𝐵
87, 1, 2wsbc 3402 . . 3 wff [𝐴 / 𝑥]𝑦𝐵
98, 5cab 2596 . 2 class {𝑦[𝐴 / 𝑥]𝑦𝐵}
104, 9wceq 1475 1 wff 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3501  csbeq1  3502  csbeq2  3503  cbvcsb  3504  csbid  3507  csbco  3509  csbtt  3510  nfcsb1d  3513  nfcsbd  3516  csbie2g  3530  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  csbprc  3932  csbprcOLD  3933  sbcel12  3935  sbceqg  3936  csbeq2d  3943  csbnestgf  3948  csbvarg  3955  csbexg  4720  bj-csbsnlem  32090  bj-csbprc  32096  csbcom2fi  33104  csbgfi  33105  sbcel12gOLD  37775
  Copyright terms: Public domain W3C validator