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 1561  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3746  df-csb 3854

This theorem is referenced by:  csbeq12dv  3862  csbco3g  4386  csbidm  4388  fmptcof  7112  mpomptsx  8045  dmmpossx  8047  fmpox  8048  ovmptss  8072  fmpoco  8074  xpf1o  9111  hsmexlem2  10395  iundom2g  10508  sumeq2ii  15730  summolem3  15751  summolem2a  15752  summo  15754  zsum  15755  fsum  15757  sumsnf  15780  fsumcnv  15810  fsumcom2  15811  fsumshftm  15818  fsum0diag2  15820  prodeq2ii  15951  prodmolem3  15973  prodmolem2a  15974  prodmo  15976  zprod  15977  fprod  15981  prodsn  16002  prodsnf  16004  fprodcnv  16023  fprodcom2  16024  bpolylem  16088  bpolyval  16089  ruclem1  16273  pcmpt  16938  gsumvalx  18720  odfval  19582  odfvalALT  19583  odval  19584  telgsumfzslem  20038  telgsumfzs  20039  rnghmval  20499  psrval  21974  psrass1lem  21992  mpfrcl  22145  evlsval  22146  evls1fval  22389  fsum2cn  24940  iunmbl2  25626  dvfsumlem1  26095  itgsubst  26118  q1pval  26222  r1pval  26225  rlimcnp2  27038  fsumdvdscom  27256  fsumdvdsmul  27266  mulsval  28209  precsexlemcbv  28306  precsexlem3  28309  fsumiunle  33037  msrfval  35892  nmulprop  36545  weiunval  36827  weiunpo  36830  weiunso  36831  weiunfr  36832  weiunse  36833  poimirlem1  38125  poimirlem3  38127  poimirlem4  38128  poimirlem5  38129  poimirlem6  38130  poimirlem7  38131  poimirlem8  38132  poimirlem10  38134  poimirlem11  38135  poimirlem12  38136  poimirlem15  38139  poimirlem16  38140  poimirlem17  38141  poimirlem18  38142  poimirlem19  38143  poimirlem20  38144  poimirlem21  38145  poimirlem22  38146  poimirlem23  38147  poimirlem24  38148  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  poimirlem28  38152  cdleme31snd  41015  cdlemeg46c  41142  cdlemkid2  41553  cdlemk46  41577  cdlemk53b  41585  cdlemk53  41586  deg1gprod  42762  fmpocos  42857  monotuz  43523  oddcomabszz  43526  fnwe2val  43631  fnwe2lem1  43632  fnwe2lem2  43633  mendval  43761  sumsnd  45597  climinf2mpt  46279  climinfmpt  46280  sge0f1o  46947  grtri  48553  dmmpossx2  48950  dfswapf2  49873