Theorem csbeq1d 3856

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

Syntax hints:   → wi 4   = wceq 1568  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3744  df-csb 3853

This theorem is referenced by:  csbeq12dv  3861  csbco3g  4395  csbidm  4397  fmptcof  7126  mpomptsx  8060  dmmpossx  8062  fmpox  8063  ovmptss  8087  fmpoco  8089  xpf1o  9126  hsmexlem2  10410  iundom2g  10523  sumeq2ii  15743  summolem3  15764  summolem2a  15765  summo  15767  zsum  15768  fsum  15770  sumsnf  15793  fsumcnv  15823  fsumcom2  15824  fsumshftm  15831  fsum0diag2  15833  prodeq2ii  15964  prodmolem3  15986  prodmolem2a  15987  prodmo  15989  zprod  15990  fprod  15994  prodsn  16015  prodsnf  16017  fprodcnv  16036  fprodcom2  16037  bpolylem  16101  bpolyval  16102  ruclem1  16286  pcmpt  16951  gsumvalx  18733  odfval  19601  odfvalALT  19602  odval  19603  telgsumfzslem  20057  telgsumfzs  20058  rnghmval  20521  psrval  22044  psrass1lem  22062  mpfrcl  22215  evlsval  22216  evls1fval  22458  fsum2cn  25009  iunmbl2  25695  dvfsumlem1  26164  itgsubst  26187  q1pval  26291  r1pval  26294  rlimcnp2  27107  fsumdvdscom  27325  fsumdvdsmul  27335  mulsval  28278  precsexlemcbv  28375  precsexlem3  28378  fsumiunle  33139  msrfval  35983  nmulprop  36636  weiunval  36917  weiunpo  36920  weiunso  36921  weiunfr  36922  weiunse  36923  poimirlem1  38216  poimirlem3  38218  poimirlem4  38219  poimirlem5  38220  poimirlem6  38221  poimirlem7  38222  poimirlem8  38223  poimirlem10  38225  poimirlem11  38226  poimirlem12  38227  poimirlem15  38230  poimirlem16  38231  poimirlem17  38232  poimirlem18  38233  poimirlem19  38234  poimirlem20  38235  poimirlem21  38236  poimirlem22  38237  poimirlem23  38238  poimirlem24  38239  poimirlem25  38240  poimirlem26  38241  poimirlem27  38242  poimirlem28  38243  cdleme31snd  41106  cdlemeg46c  41233  cdlemkid2  41644  cdlemk46  41668  cdlemk53b  41676  cdlemk53  41677  deg1gprod  42853  fmpocos  42950  monotuz  43616  oddcomabszz  43619  fnwe2val  43724  fnwe2lem1  43725  fnwe2lem2  43726  mendval  43854  sumsnd  45694  climinf2mpt  46376  climinfmpt  46377  sge0f1o  47044  grtri  48650  dmmpossx2  49062  dfswapf2  49984