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

Theorem csbied 3893
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.)
Hypotheses
Ref Expression
csbied.1 (𝜑𝐴𝑉)
csbied.2 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
Assertion
Ref Expression
csbied (𝜑𝐴 / 𝑥𝐵 = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem csbied
StepHypRef Expression
1 nfv 1916 . 2 𝑥𝜑
2 nfcvd 2975 . 2 (𝜑𝑥𝐶)
3 csbied.1 . 2 (𝜑𝐴𝑉)
4 csbied.2 . 2 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
51, 2, 3, 4csbiedf 3887 1 (𝜑𝐴 / 𝑥𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2115  csb 3857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-v 3473  df-sbc 3750  df-csb 3858
This theorem is referenced by:  csbied2  3894  rspc2vd  3906  el2mpocl  7756  mposn  7773  cantnfval  9107  fprodeq0  15308  imasval  16763  gsumvalx  17865  efmnd  18014  mulgfval  18205  mulgfvalALT  18206  isga  18400  gexval  18682  telgsumfz  19089  telgsumfz0  19091  telgsum  19093  isirred  19428  psrval  20118  mplval  20184  opsrval  20231  evlsval  20275  evls1fval  20458  evl1fval  20467  znval  20658  scmatval  21089  pmatcollpw3lem  21367  pm2mpval  21379  pm2mpmhmlem2  21403  chfacffsupp  21440  tsmsval2  22714  dvfsumle  24603  dvfsumabs  24605  dvfsumlem1  24608  dvfsum2  24616  itgparts  24629  q1pval  24733  r1pval  24736  rlimcnp2  25531  vmaval  25677  fsumdvdscom  25749  fsumvma  25776  logexprlim  25788  dchrval  25797  dchrisumlema  26051  dchrisumlem2  26053  dchrisumlem3  26054  ttgval  26648  finsumvtxdg2sstep  27318  msrval  32793  poimirlem1  34940  poimirlem2  34941  poimirlem6  34945  poimirlem7  34946  poimirlem10  34949  poimirlem11  34950  poimirlem12  34951  poimirlem23  34962  poimirlem24  34963  fsumshftd  36130  hlhilset  39112  prjspval  39404  mendval  39934  ply1mulgsumlem3  44614  ply1mulgsumlem4  44615  ply1mulgsum  44616  dmatALTval  44627
  Copyright terms: Public domain W3C validator