Theorem csbeq1d 3788

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 3784	. 2 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1508  ⦋csb 3781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-sbc 3677  df-csb 3782

This theorem is referenced by:  csbco3g  4259  csbidm  4261  fmptcof  6714  mpomptsx  7569  dmmpossx  7571  fmpox  7572  ovmptss  7595  fmpoco  7597  xpf1o  8474  hsmexlem2  9646  iundom2g  9759  sumeq2ii  14909  summolem3  14930  summolem2a  14931  summo  14933  zsum  14934  fsum  14936  sumsnf  14958  fsumcnv  14987  fsumcom2  14988  fsumshftm  14995  fsum0diag2  14997  prodeq2ii  15126  prodmolem3  15146  prodmolem2a  15147  prodmo  15149  zprod  15150  fprod  15154  prodsn  15175  prodsnf  15177  fprodcnv  15196  fprodcom2  15197  bpolylem  15261  bpolyval  15262  ruclem1  15443  pcmpt  16083  gsumvalx  17751  odfval  18435  odfvalALT  18436  odval  18437  telgsumfzslem  18871  telgsumfzs  18872  psrval  19869  psrass1lem  19884  mpfrcl  20024  evlsval  20025  evls1fval  20201  fsum2cn  23198  iunmbl2  23877  dvfsumlem1  24342  itgsubst  24365  q1pval  24466  r1pval  24469  rlimcnp2  25262  fsumdvdscom  25480  fsumdvdsmul  25490  ttgval  26380  fsumiunle  30316  msrfval  32337  poimirlem1  34367  poimirlem3  34369  poimirlem4  34370  poimirlem5  34371  poimirlem6  34372  poimirlem7  34373  poimirlem8  34374  poimirlem10  34376  poimirlem11  34377  poimirlem12  34378  poimirlem15  34381  poimirlem16  34382  poimirlem17  34383  poimirlem18  34384  poimirlem19  34385  poimirlem20  34386  poimirlem21  34387  poimirlem22  34388  poimirlem23  34389  poimirlem24  34390  poimirlem25  34391  poimirlem26  34392  poimirlem27  34393  poimirlem28  34394  cdleme31snd  37000  cdlemeg46c  37127  cdlemkid2  37538  cdlemk46  37562  cdlemk53b  37570  cdlemk53  37571  monotuz  38968  oddcomabszz  38971  fnwe2val  39079  fnwe2lem1  39080  fnwe2lem2  39081  mendval  39213  sumsnd  40736  climinf2mpt  41456  climinfmpt  41457  sge0f1o  42125  rnghmval  43556  dmmpossx2  43779