Theorem csbeq1d 3857

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

Syntax hints:   → wi 4   = wceq 1540  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3745  df-csb 3854

This theorem is referenced by:  csbeq12dv  3862  csbco3g  4384  csbidm  4386  fmptcof  7068  mpomptsx  8006  dmmpossx  8008  fmpox  8009  ovmptss  8033  fmpoco  8035  xpf1o  9063  hsmexlem2  10340  iundom2g  10453  sumeq2ii  15618  summolem3  15639  summolem2a  15640  summo  15642  zsum  15643  fsum  15645  sumsnf  15668  fsumcnv  15698  fsumcom2  15699  fsumshftm  15706  fsum0diag2  15708  prodeq2ii  15836  prodmolem3  15858  prodmolem2a  15859  prodmo  15861  zprod  15862  fprod  15866  prodsn  15887  prodsnf  15889  fprodcnv  15908  fprodcom2  15909  bpolylem  15973  bpolyval  15974  ruclem1  16158  pcmpt  16822  gsumvalx  18568  odfval  19429  odfvalALT  19430  odval  19431  telgsumfzslem  19885  telgsumfzs  19886  rnghmval  20343  psrval  21840  psrass1lem  21857  mpfrcl  22008  evlsval  22009  evls1fval  22222  fsum2cn  24778  iunmbl2  25474  dvfsumlem1  25948  itgsubst  25972  q1pval  26076  r1pval  26079  rlimcnp2  26892  fsumdvdscom  27111  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  mulsval  28035  precsexlemcbv  28131  precsexlem3  28134  fsumiunle  32787  msrfval  35509  weiunlem1  36435  weiunpo  36438  weiunso  36439  weiunfr  36440  weiunse  36441  poimirlem1  37600  poimirlem3  37602  poimirlem4  37603  poimirlem5  37604  poimirlem6  37605  poimirlem7  37606  poimirlem8  37607  poimirlem10  37609  poimirlem11  37610  poimirlem12  37611  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  poimirlem21  37620  poimirlem22  37621  poimirlem23  37622  poimirlem24  37623  poimirlem25  37624  poimirlem26  37625  poimirlem27  37626  poimirlem28  37627  cdleme31snd  40365  cdlemeg46c  40492  cdlemkid2  40903  cdlemk46  40927  cdlemk53b  40935  cdlemk53  40936  deg1gprod  42113  fmpocos  42207  monotuz  42914  oddcomabszz  42917  fnwe2val  43022  fnwe2lem1  43023  fnwe2lem2  43024  mendval  43152  sumsnd  45004  climinf2mpt  45696  climinfmpt  45697  sge0f1o  46364  grtri  47923  dmmpossx2  48309  dfswapf2  49234