Theorem csbeq1d 3925

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

Syntax hints:   → wi 4   = wceq 1537  ⦋csb 3921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805  df-csb 3922

This theorem is referenced by:  csbeq12dv  3930  csbco3g  4454  csbidm  4456  fmptcof  7164  mpomptsx  8105  dmmpossx  8107  fmpox  8108  ovmptss  8134  fmpoco  8136  xpf1o  9205  hsmexlem2  10496  iundom2g  10609  sumeq2ii  15741  summolem3  15762  summolem2a  15763  summo  15765  zsum  15766  fsum  15768  sumsnf  15791  fsumcnv  15821  fsumcom2  15822  fsumshftm  15829  fsum0diag2  15831  prodeq2ii  15959  prodmolem3  15981  prodmolem2a  15982  prodmo  15984  zprod  15985  fprod  15989  prodsn  16010  prodsnf  16012  fprodcnv  16031  fprodcom2  16032  bpolylem  16096  bpolyval  16097  ruclem1  16279  pcmpt  16939  gsumvalx  18714  odfval  19574  odfvalALT  19575  odval  19576  telgsumfzslem  20030  telgsumfzs  20031  rnghmval  20466  psrval  21958  psrass1lem  21975  mpfrcl  22132  evlsval  22133  evls1fval  22344  fsum2cn  24914  iunmbl2  25611  dvfsumlem1  26086  itgsubst  26110  q1pval  26214  r1pval  26217  rlimcnp2  27027  fsumdvdscom  27246  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  mulsval  28153  precsexlemcbv  28248  precsexlem3  28251  ttgvalOLD  28902  fsumiunle  32833  msrfval  35505  weiunlem1  36428  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  poimirlem1  37581  poimirlem3  37583  poimirlem4  37584  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem28  37608  cdleme31snd  40343  cdlemeg46c  40470  cdlemkid2  40881  cdlemk46  40905  cdlemk53b  40913  cdlemk53  40914  deg1gprod  42097  fmpocos  42229  monotuz  42898  oddcomabszz  42901  fnwe2val  43006  fnwe2lem1  43007  fnwe2lem2  43008  mendval  43140  sumsnd  44926  climinf2mpt  45635  climinfmpt  45636  sge0f1o  46303  grtri  47791  dmmpossx2  48061