Theorem csbeq1d 3849

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

Syntax hints:   → wi 4   = wceq 1541  ⦋csb 3845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sbc 3737  df-csb 3846

This theorem is referenced by:  csbeq12dv  3854  csbco3g  4380  csbidm  4382  fmptcof  7069  mpomptsx  8002  dmmpossx  8004  fmpox  8005  ovmptss  8029  fmpoco  8031  xpf1o  9058  hsmexlem2  10324  iundom2g  10437  sumeq2ii  15606  summolem3  15627  summolem2a  15628  summo  15630  zsum  15631  fsum  15633  sumsnf  15656  fsumcnv  15686  fsumcom2  15687  fsumshftm  15694  fsum0diag2  15696  prodeq2ii  15824  prodmolem3  15846  prodmolem2a  15847  prodmo  15849  zprod  15850  fprod  15854  prodsn  15875  prodsnf  15877  fprodcnv  15896  fprodcom2  15897  bpolylem  15961  bpolyval  15962  ruclem1  16146  pcmpt  16810  gsumvalx  18590  odfval  19450  odfvalALT  19451  odval  19452  telgsumfzslem  19906  telgsumfzs  19907  rnghmval  20364  psrval  21858  psrass1lem  21875  mpfrcl  22026  evlsval  22027  evls1fval  22240  fsum2cn  24795  iunmbl2  25491  dvfsumlem1  25965  itgsubst  25989  q1pval  26093  r1pval  26096  rlimcnp2  26909  fsumdvdscom  27128  fsumdvdsmul  27138  fsumdvdsmulOLD  27140  mulsval  28054  precsexlemcbv  28150  precsexlem3  28153  fsumiunle  32819  msrfval  35588  weiunlem1  36513  weiunpo  36516  weiunso  36517  weiunfr  36518  weiunse  36519  poimirlem1  37667  poimirlem3  37669  poimirlem4  37670  poimirlem5  37671  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem18  37684  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem26  37692  poimirlem27  37693  poimirlem28  37694  cdleme31snd  40491  cdlemeg46c  40618  cdlemkid2  41029  cdlemk46  41053  cdlemk53b  41061  cdlemk53  41062  deg1gprod  42239  fmpocos  42333  monotuz  43039  oddcomabszz  43042  fnwe2val  43147  fnwe2lem1  43148  fnwe2lem2  43149  mendval  43277  sumsnd  45128  climinf2mpt  45817  climinfmpt  45818  sge0f1o  46485  grtri  48045  dmmpossx2  48442  dfswapf2  49367