Theorem csbeq1d 3898

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

Syntax hints:   → wi 4   = wceq 1533  ⦋csb 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-sbc 3779  df-csb 3895

This theorem is referenced by:  csbeq12dv  3903  csbco3g  4432  csbidm  4434  fmptcof  7145  mpomptsx  8074  dmmpossx  8076  fmpox  8077  ovmptss  8104  fmpoco  8106  xpf1o  9170  hsmexlem2  10458  iundom2g  10571  sumeq2ii  15679  summolem3  15700  summolem2a  15701  summo  15703  zsum  15704  fsum  15706  sumsnf  15729  fsumcnv  15759  fsumcom2  15760  fsumshftm  15767  fsum0diag2  15769  prodeq2ii  15897  prodmolem3  15917  prodmolem2a  15918  prodmo  15920  zprod  15921  fprod  15925  prodsn  15946  prodsnf  15948  fprodcnv  15967  fprodcom2  15968  bpolylem  16032  bpolyval  16033  ruclem1  16215  pcmpt  16868  gsumvalx  18643  odfval  19494  odfvalALT  19495  odval  19496  telgsumfzslem  19950  telgsumfzs  19951  rnghmval  20386  psrval  21855  psrass1lemOLD  21881  psrass1lem  21884  mpfrcl  22038  evlsval  22039  evls1fval  22245  fsum2cn  24809  iunmbl2  25506  dvfsumlem1  25980  itgsubst  26004  q1pval  26110  r1pval  26113  rlimcnp2  26918  fsumdvdscom  27137  fsumdvdsmul  27147  fsumdvdsmulOLD  27149  mulsval  28029  precsexlemcbv  28124  precsexlem3  28127  ttgvalOLD  28700  fsumiunle  32613  msrfval  35180  poimirlem1  37127  poimirlem3  37129  poimirlem4  37130  poimirlem5  37131  poimirlem6  37132  poimirlem7  37133  poimirlem8  37134  poimirlem10  37136  poimirlem11  37137  poimirlem12  37138  poimirlem15  37141  poimirlem16  37142  poimirlem17  37143  poimirlem18  37144  poimirlem19  37145  poimirlem20  37146  poimirlem21  37147  poimirlem22  37148  poimirlem23  37149  poimirlem24  37150  poimirlem25  37151  poimirlem26  37152  poimirlem27  37153  poimirlem28  37154  cdleme31snd  39891  cdlemeg46c  40018  cdlemkid2  40429  cdlemk46  40453  cdlemk53b  40461  cdlemk53  40462  deg1gprod  41644  fmpocos  41756  monotuz  42393  oddcomabszz  42396  fnwe2val  42504  fnwe2lem1  42505  fnwe2lem2  42506  mendval  42638  sumsnd  44419  climinf2mpt  45131  climinfmpt  45132  sge0f1o  45799  dmmpossx2  47478