MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  csbie Structured version   Visualization version   GIF version

Theorem csbie 3944
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by AV, 2-Dec-2019.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.)
Hypotheses
Ref Expression
csbie.1 𝐴 ∈ V
csbie.2 (𝑥 = 𝐴𝐵 = 𝐶)
Assertion
Ref Expression
csbie 𝐴 / 𝑥𝐵 = 𝐶
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem csbie
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-csb 3909 . 2 𝐴 / 𝑥𝐵 = {𝑦[𝐴 / 𝑥]𝑦𝐵}
2 csbie.1 . . . 4 𝐴 ∈ V
3 csbie.2 . . . . 5 (𝑥 = 𝐴𝐵 = 𝐶)
43eleq2d 2825 . . . 4 (𝑥 = 𝐴 → (𝑦𝐵𝑦𝐶))
52, 4sbcie 3835 . . 3 ([𝐴 / 𝑥]𝑦𝐵𝑦𝐶)
65abbii 2807 . 2 {𝑦[𝐴 / 𝑥]𝑦𝐵} = {𝑦𝑦𝐶}
7 abid2 2877 . 2 {𝑦𝑦𝐶} = 𝐶
81, 6, 73eqtri 2767 1 𝐴 / 𝑥𝐵 = 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  wcel 2106  {cab 2712  Vcvv 3478  [wsbc 3791  csb 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792  df-csb 3909
This theorem is referenced by:  pofun  5615  eqerlem  8779  mptnn0fsuppd  14036  fsum  15753  fsumcnv  15806  fsumshftm  15814  fsum0diag2  15816  fprod  15974  fprodcnv  16016  bpolyval  16082  ruclem1  16264  odfval  19565  odval  19567  psrass1lem  21970  selvval  22157  mamufval  22412  pm2mpval  22817  isibl  25815  dfitg  25819  dvfsumlem2  26082  dvfsumlem2OLD  26083  fsumdvdsmul  27253  fsumdvdsmulOLD  27255  precsexlem3  28248  disjxpin  32608  poimirlem1  37608  poimirlem5  37612  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem22  37629  poimirlem24  37631  poimirlem28  37635  evlselv  42574  fphpd  42804  monotuz  42930  oddcomabszz  42933  fnwe2val  43038  fnwe2lem1  43039
  Copyright terms: Public domain W3C validator