Theorem csbeq1d 3866

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

Syntax hints:   → wi 4   = wceq 1540  ⦋csb 3862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3754  df-csb 3863

This theorem is referenced by:  csbeq12dv  3871  csbco3g  4394  csbidm  4396  fmptcof  7102  mpomptsx  8043  dmmpossx  8045  fmpox  8046  ovmptss  8072  fmpoco  8074  xpf1o  9103  hsmexlem2  10380  iundom2g  10493  sumeq2ii  15659  summolem3  15680  summolem2a  15681  summo  15683  zsum  15684  fsum  15686  sumsnf  15709  fsumcnv  15739  fsumcom2  15740  fsumshftm  15747  fsum0diag2  15749  prodeq2ii  15877  prodmolem3  15899  prodmolem2a  15900  prodmo  15902  zprod  15903  fprod  15907  prodsn  15928  prodsnf  15930  fprodcnv  15949  fprodcom2  15950  bpolylem  16014  bpolyval  16015  ruclem1  16199  pcmpt  16863  gsumvalx  18603  odfval  19462  odfvalALT  19463  odval  19464  telgsumfzslem  19918  telgsumfzs  19919  rnghmval  20349  psrval  21824  psrass1lem  21841  mpfrcl  21992  evlsval  21993  evls1fval  22206  fsum2cn  24762  iunmbl2  25458  dvfsumlem1  25932  itgsubst  25956  q1pval  26060  r1pval  26063  rlimcnp2  26876  fsumdvdscom  27095  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  mulsval  28012  precsexlemcbv  28108  precsexlem3  28111  fsumiunle  32754  msrfval  35524  weiunlem1  36450  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  poimirlem1  37615  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  cdleme31snd  40380  cdlemeg46c  40507  cdlemkid2  40918  cdlemk46  40942  cdlemk53b  40950  cdlemk53  40951  deg1gprod  42128  fmpocos  42222  monotuz  42930  oddcomabszz  42933  fnwe2val  43038  fnwe2lem1  43039  fnwe2lem2  43040  mendval  43168  sumsnd  45020  climinf2mpt  45712  climinfmpt  45713  sge0f1o  46380  grtri  47939  dmmpossx2  48325  dfswapf2  49250