Theorem csbeq1d 3847

Description: Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)

Hypothesis

Ref	Expression
csbeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
csbeq1d	⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Proof of Theorem csbeq1d

Step	Hyp	Ref	Expression
1		csbeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		csbeq1 3846	. 2 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1550  ⦋csb 3843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-sbc 3736  df-csb 3844

This theorem is referenced by:  csbeq12dv  3852  csbco3g  4375  csbidm  4377  fmptcof  7097  mpomptsx  8030  dmmpossx  8032  fmpox  8033  ovmptss  8056  fmpoco  8058  xpf1o  9096  hsmexlem2  10370  iundom2g  10483  sumeq2ii  15692  summolem3  15713  summolem2a  15714  summo  15716  zsum  15717  fsum  15719  sumsnf  15742  fsumcnv  15772  fsumcom2  15773  fsumshftm  15780  fsum0diag2  15782  prodeq2ii  15913  prodmolem3  15935  prodmolem2a  15936  prodmo  15938  zprod  15939  fprod  15943  prodsn  15964  prodsnf  15966  fprodcnv  15985  fprodcom2  15986  bpolylem  16050  bpolyval  16051  ruclem1  16235  pcmpt  16900  gsumvalx  18682  odfval  19544  odfvalALT  19545  odval  19546  telgsumfzslem  20000  telgsumfzs  20001  rnghmval  20457  psrval  21936  psrass1lem  21954  mpfrcl  22107  evlsval  22108  evls1fval  22351  fsum2cn  24902  iunmbl2  25588  dvfsumlem1  26057  itgsubst  26080  q1pval  26184  r1pval  26187  rlimcnp2  26997  fsumdvdscom  27215  fsumdvdsmul  27225  mulsval  28168  precsexlemcbv  28265  precsexlem3  28268  fsumiunle  32970  msrfval  35825  nmulprop  36478  weiunval  36760  weiunpo  36763  weiunso  36764  weiunfr  36765  weiunse  36766  poimirlem1  38058  poimirlem3  38060  poimirlem4  38061  poimirlem5  38062  poimirlem6  38063  poimirlem7  38064  poimirlem8  38065  poimirlem10  38067  poimirlem11  38068  poimirlem12  38069  poimirlem15  38072  poimirlem16  38073  poimirlem17  38074  poimirlem18  38075  poimirlem19  38076  poimirlem20  38077  poimirlem21  38078  poimirlem22  38079  poimirlem23  38080  poimirlem24  38081  poimirlem25  38082  poimirlem26  38083  poimirlem27  38084  poimirlem28  38085  cdleme31snd  40948  cdlemeg46c  41075  cdlemkid2  41486  cdlemk46  41510  cdlemk53b  41518  cdlemk53  41519  deg1gprod  42695  fmpocos  42790  monotuz  43456  oddcomabszz  43459  fnwe2val  43564  fnwe2lem1  43565  fnwe2lem2  43566  mendval  43694  sumsnd  45544  climinf2mpt  46226  climinfmpt  46227  sge0f1o  46894  grtri  48500  dmmpossx2  48897  dfswapf2  49820