Theorem csbeq1d 3505

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

Syntax hints:   → wi 4   = wceq 1474  ⦋csb 3498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-sbc 3402  df-csb 3499

This theorem is referenced by:  csbco3g  3951  csbidm  3953  fmptcof  6289  mpt2mptsx  7100  dmmpt2ssx  7102  fmpt2x  7103  ovmptss  7123  fmpt2co  7125  xpf1o  7985  hsmexlem2  9110  iundom2g  9219  sumeq2ii  14220  summolem3  14241  summolem2a  14242  summo  14244  zsum  14245  fsum  14247  sumsn  14268  fsumcnv  14295  fsumcom2  14296  fsumcom2OLD  14297  fsumshftm  14304  fsum0diag2  14306  prodeq2ii  14431  prodmolem3  14451  prodmolem2a  14452  prodmo  14454  zprod  14455  fprod  14459  prodsn  14480  prodsnf  14482  fprodcnv  14501  fprodcom2  14502  fprodcom2OLD  14503  bpolylem  14567  bpolyval  14568  ruclem1  14748  pcmpt  15383  gsumvalx  17042  odfval  17724  odval  17725  telgsumfzslem  18157  telgsumfzs  18158  psrval  19132  psrass1lem  19147  mpfrcl  19288  evlsval  19289  evls1fval  19454  fsum2cn  22430  iunmbl2  23077  dvfsumlem1  23538  itgsubst  23561  q1pval  23662  r1pval  23665  rlimcnp2  24438  fsumdvdscom  24656  fsumdvdsmul  24666  ttgval  25501  msrfval  30522  poimirlem1  32404  poimirlem3  32406  poimirlem4  32407  poimirlem5  32408  poimirlem6  32409  poimirlem7  32410  poimirlem8  32411  poimirlem10  32413  poimirlem11  32414  poimirlem12  32415  poimirlem15  32418  poimirlem16  32419  poimirlem17  32420  poimirlem18  32421  poimirlem19  32422  poimirlem20  32423  poimirlem21  32424  poimirlem22  32425  poimirlem23  32426  poimirlem24  32427  poimirlem25  32428  poimirlem26  32429  poimirlem27  32430  poimirlem28  32431  fsumshftdOLD  33080  cdleme31snd  34516  cdlemeg46c  34643  cdlemkid2  35054  cdlemk46  35078  cdlemk53b  35086  cdlemk53  35087  monotuz  36348  oddcomabszz  36351  fnwe2val  36461  fnwe2lem1  36462  fnwe2lem2  36463  mendval  36596  sumsnd  38032  sumsnf  38460  sge0f1o  39099  rnghmval  41703  dmmpt2ssx2  41930