Theorem csbeq1d 3911

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

Syntax hints:   → wi 4   = wceq 1536  ⦋csb 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-sbc 3791  df-csb 3908

This theorem is referenced by:  csbeq12dv  3916  csbco3g  4436  csbidm  4438  fmptcof  7149  mpomptsx  8087  dmmpossx  8089  fmpox  8090  ovmptss  8116  fmpoco  8118  xpf1o  9177  hsmexlem2  10464  iundom2g  10577  sumeq2ii  15725  summolem3  15746  summolem2a  15747  summo  15749  zsum  15750  fsum  15752  sumsnf  15775  fsumcnv  15805  fsumcom2  15806  fsumshftm  15813  fsum0diag2  15815  prodeq2ii  15943  prodmolem3  15965  prodmolem2a  15966  prodmo  15968  zprod  15969  fprod  15973  prodsn  15994  prodsnf  15996  fprodcnv  16015  fprodcom2  16016  bpolylem  16080  bpolyval  16081  ruclem1  16263  pcmpt  16925  gsumvalx  18701  odfval  19564  odfvalALT  19565  odval  19566  telgsumfzslem  20020  telgsumfzs  20021  rnghmval  20456  psrval  21952  psrass1lem  21969  mpfrcl  22126  evlsval  22127  evls1fval  22338  fsum2cn  24908  iunmbl2  25605  dvfsumlem1  26080  itgsubst  26104  q1pval  26208  r1pval  26211  rlimcnp2  27023  fsumdvdscom  27242  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  mulsval  28149  precsexlemcbv  28244  precsexlem3  28247  ttgvalOLD  28898  fsumiunle  32835  msrfval  35521  weiunlem1  36444  weiunpo  36447  weiunso  36448  weiunfr  36449  weiunse  36450  poimirlem1  37607  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  cdleme31snd  40368  cdlemeg46c  40495  cdlemkid2  40906  cdlemk46  40930  cdlemk53b  40938  cdlemk53  40939  deg1gprod  42121  fmpocos  42253  monotuz  42929  oddcomabszz  42932  fnwe2val  43037  fnwe2lem1  43038  fnwe2lem2  43039  mendval  43167  sumsnd  44963  climinf2mpt  45669  climinfmpt  45670  sge0f1o  46337  grtri  47844  dmmpossx2  48181