Theorem csbeq1d 3850

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbeq12dv  3855  csbco3g  4388  csbidm  4390  fmptcof  7119  mpomptsx  8058  dmmpossx  8060  fmpox  8061  ovmptss  8087  fmpoco  8089  xpf1o  9136  hsmexlem2  10476  iundom2g  10595  sumeq2ii  15827  summolem3  15847  summolem2a  15848  summo  15850  zsum  15851  fsum  15853  sumsnf  15876  fsumcnv  15906  fsumcom2  15907  fsumshftm  15914  fsum0diag2  15916  prodeq2ii  16047  prodmolem3  16067  prodmolem2a  16068  prodmo  16070  zprod  16071  fprod  16075  prodsn  16096  prodsnf  16098  fprodcnv  16117  fprodcom2  16118  bpolylem  16181  bpolyval  16182  ruclem1  16366  pcmpt  17031  gsumvalx  18826  odfval  19707  odfvalALT  19708  odval  19709  telgsumfzslem  20163  telgsumfzs  20164  rnghmval  20631  rhmval0  20666  psrval  22184  psrass1lem  22202  mpfrcl  22355  evlsval  22356  evls1fval  22598  fsum2cn  25153  iunmbl2  25839  dvfsumlem1  26307  itgsubst  26330  q1pval  26434  r1pval  26437  rlimcnp2  27257  fsumdvdscom  27475  fsumdvdsmul  27485  mulsval  28428  precsexlemcbv  28525  precsexlem3  28528  fsumiunle  33353  msrfval  36223  nmulprop  36861  weiunval  37172  weiunpo  37175  weiunso  37176  weiunfr  37177  weiunse  37178  poimirlem1  38459  poimirlem3  38461  poimirlem4  38462  poimirlem5  38463  poimirlem6  38464  poimirlem7  38465  poimirlem8  38466  poimirlem10  38468  poimirlem11  38469  poimirlem12  38470  poimirlem15  38473  poimirlem16  38474  poimirlem17  38475  poimirlem18  38476  poimirlem19  38477  poimirlem20  38478  poimirlem21  38479  poimirlem22  38480  poimirlem23  38481  poimirlem24  38482  poimirlem25  38483  poimirlem26  38484  poimirlem27  38485  poimirlem28  38486  cdleme31snd  41363  cdlemeg46c  41490  cdlemkid2  41901  cdlemk46  41925  cdlemk53b  41933  cdlemk53  41934  deg1gprod  43110  fmpocos  43207  monotuz  43886  oddcomabszz  43889  fnwe2val  43994  fnwe2lem1  43995  fnwe2lem2  43996  mendval  44124  sumsnd  45964  climinf2mpt  46646  climinfmpt  46647  sge0f1o  47314  grtri  48960  dmmpossx2  49371  dfswapf2  50291