Theorem csbeq1d 3837

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

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

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-sbc 3726  df-csb 3834

This theorem is referenced by:  csbeq12dv  3842  csbco3g  4361  csbidm  4363  fmptcof  7072  mpomptsx  8006  dmmpossx  8008  fmpox  8009  ovmptss  8032  fmpoco  8034  xpf1o  9066  hsmexlem2  10338  iundom2g  10451  sumeq2ii  15644  summolem3  15665  summolem2a  15666  summo  15668  zsum  15669  fsum  15671  sumsnf  15694  fsumcnv  15724  fsumcom2  15725  fsumshftm  15732  fsum0diag2  15734  prodeq2ii  15865  prodmolem3  15887  prodmolem2a  15888  prodmo  15890  zprod  15891  fprod  15895  prodsn  15916  prodsnf  15918  fprodcnv  15937  fprodcom2  15938  bpolylem  16002  bpolyval  16003  ruclem1  16187  pcmpt  16852  gsumvalx  18633  odfval  19496  odfvalALT  19497  odval  19498  telgsumfzslem  19952  telgsumfzs  19953  rnghmval  20409  psrval  21884  psrass1lem  21901  mpfrcl  22052  evlsval  22053  evls1fval  22272  fsum2cn  24826  iunmbl2  25512  dvfsumlem1  25981  itgsubst  26004  q1pval  26108  r1pval  26111  rlimcnp2  26918  fsumdvdscom  27136  fsumdvdsmul  27146  mulsval  28089  precsexlemcbv  28186  precsexlem3  28189  fsumiunle  32890  msrfval  35707  weiunval  36632  weiunpo  36635  weiunso  36636  weiunfr  36637  weiunse  36638  poimirlem1  37930  poimirlem3  37932  poimirlem4  37933  poimirlem5  37934  poimirlem6  37935  poimirlem7  37936  poimirlem8  37937  poimirlem10  37939  poimirlem11  37940  poimirlem12  37941  poimirlem15  37944  poimirlem16  37945  poimirlem17  37946  poimirlem18  37947  poimirlem19  37948  poimirlem20  37949  poimirlem21  37950  poimirlem22  37951  poimirlem23  37952  poimirlem24  37953  poimirlem25  37954  poimirlem26  37955  poimirlem27  37956  poimirlem28  37957  cdleme31snd  40820  cdlemeg46c  40947  cdlemkid2  41358  cdlemk46  41382  cdlemk53b  41390  cdlemk53  41391  deg1gprod  42567  fmpocos  42663  monotuz  43357  oddcomabszz  43360  fnwe2val  43465  fnwe2lem1  43466  fnwe2lem2  43467  mendval  43595  sumsnd  45445  climinf2mpt  46130  climinfmpt  46131  sge0f1o  46798  grtri  48404  dmmpossx2  48801  dfswapf2  49724