Theorem csbeq1d 3898

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

Syntax hints:   → wi 4   = wceq 1542  ⦋csb 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779  df-csb 3895

This theorem is referenced by:  csbeq12dv  3903  csbco3g  4429  csbidm  4431  fmptcof  7128  mpomptsx  8050  dmmpossx  8052  fmpox  8053  ovmptss  8079  fmpoco  8081  xpf1o  9139  hsmexlem2  10422  iundom2g  10535  sumeq2ii  15639  summolem3  15660  summolem2a  15661  summo  15663  zsum  15664  fsum  15666  sumsnf  15689  fsumcnv  15719  fsumcom2  15720  fsumshftm  15727  fsum0diag2  15729  prodeq2ii  15857  prodmolem3  15877  prodmolem2a  15878  prodmo  15880  zprod  15881  fprod  15885  prodsn  15906  prodsnf  15908  fprodcnv  15927  fprodcom2  15928  bpolylem  15992  bpolyval  15993  ruclem1  16174  pcmpt  16825  gsumvalx  18595  odfval  19400  odfvalALT  19401  odval  19402  telgsumfzslem  19856  telgsumfzs  19857  psrval  21468  psrass1lemOLD  21493  psrass1lem  21496  mpfrcl  21648  evlsval  21649  evls1fval  21838  fsum2cn  24387  iunmbl2  25074  dvfsumlem1  25543  itgsubst  25566  q1pval  25671  r1pval  25674  rlimcnp2  26471  fsumdvdscom  26689  fsumdvdsmul  26699  mulsval  27565  precsexlemcbv  27652  precsexlem3  27655  ttgvalOLD  28127  fsumiunle  32035  msrfval  34528  poimirlem1  36489  poimirlem3  36491  poimirlem4  36492  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  cdleme31snd  39257  cdlemeg46c  39384  cdlemkid2  39795  cdlemk46  39819  cdlemk53b  39827  cdlemk53  39828  fmpocos  41056  monotuz  41680  oddcomabszz  41683  fnwe2val  41791  fnwe2lem1  41792  fnwe2lem2  41793  mendval  41925  sumsnd  43710  climinf2mpt  44430  climinfmpt  44431  sge0f1o  45098  rnghmval  46689  dmmpossx2  47012