Theorem csbeq1d 3854

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⦋csb 3850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743  df-csb 3851

This theorem is used by:  csbeq12dv  3859  csbco3g  4392  csbidm  4394  fmptcof  7127  mpomptsx  8064  dmmpossx  8066  fmpox  8067  ovmptss  8093  fmpoco  8095  xpf1o  9140  hsmexlem2  10432  iundom2g  10551  sumeq2ii  15782  summolem3  15802  summolem2a  15803  summo  15805  zsum  15806  fsum  15808  sumsnf  15831  fsumcnv  15861  fsumcom2  15862  fsumshftm  15869  fsum0diag2  15871  prodeq2ii  16002  prodmolem3  16024  prodmolem2a  16025  prodmo  16027  zprod  16028  fprod  16032  prodsn  16053  prodsnf  16055  fprodcnv  16074  fprodcom2  16075  bpolylem  16138  bpolyval  16139  ruclem1  16323  pcmpt  16988  gsumvalx  18780  odfval  19660  odfvalALT  19661  odval  19662  telgsumfzslem  20116  telgsumfzs  20117  rnghmval  20582  rhmval0  20617  psrval  22131  psrass1lem  22149  mpfrcl  22302  evlsval  22303  evls1fval  22545  fsum2cn  25100  iunmbl2  25786  dvfsumlem1  26255  itgsubst  26278  q1pval  26382  r1pval  26385  rlimcnp2  27201  fsumdvdscom  27419  fsumdvdsmul  27429  mulsval  28372  precsexlemcbv  28469  precsexlem3  28472  fsumiunle  33286  msrfval  36103  nmulprop  36757  weiunval  37068  weiunpo  37071  weiunso  37072  weiunfr  37073  weiunse  37074  poimirlem1  38357  poimirlem3  38359  poimirlem4  38360  poimirlem5  38361  poimirlem6  38362  poimirlem7  38363  poimirlem8  38364  poimirlem10  38366  poimirlem11  38367  poimirlem12  38368  poimirlem15  38371  poimirlem16  38372  poimirlem17  38373  poimirlem18  38374  poimirlem19  38375  poimirlem20  38376  poimirlem21  38377  poimirlem22  38378  poimirlem23  38379  poimirlem24  38380  poimirlem25  38381  poimirlem26  38382  poimirlem27  38383  poimirlem28  38384  cdleme31snd  41246  cdlemeg46c  41373  cdlemkid2  41784  cdlemk46  41808  cdlemk53b  41816  cdlemk53  41817  deg1gprod  42993  fmpocos  43090  monotuz  43769  oddcomabszz  43772  fnwe2val  43877  fnwe2lem1  43878  fnwe2lem2  43879  mendval  44007  sumsnd  45847  climinf2mpt  46529  climinfmpt  46530  sge0f1o  47197  grtri  48843  dmmpossx2  49254  dfswapf2  50174