Theorem csbeq1d 3832

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

Syntax hints:   → wi 4   = wceq 1539  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712  df-csb 3829

This theorem is referenced by:  csbeq12dv  3837  csbco3g  4359  csbidm  4361  fmptcof  6984  mpomptsx  7877  dmmpossx  7879  fmpox  7880  ovmptss  7904  fmpoco  7906  xpf1o  8875  hsmexlem2  10114  iundom2g  10227  sumeq2ii  15333  summolem3  15354  summolem2a  15355  summo  15357  zsum  15358  fsum  15360  sumsnf  15383  fsumcnv  15413  fsumcom2  15414  fsumshftm  15421  fsum0diag2  15423  prodeq2ii  15551  prodmolem3  15571  prodmolem2a  15572  prodmo  15574  zprod  15575  fprod  15579  prodsn  15600  prodsnf  15602  fprodcnv  15621  fprodcom2  15622  bpolylem  15686  bpolyval  15687  ruclem1  15868  pcmpt  16521  gsumvalx  18275  odfval  19055  odfvalALT  19056  odval  19057  telgsumfzslem  19504  telgsumfzs  19505  psrval  21028  psrass1lemOLD  21053  psrass1lem  21056  mpfrcl  21205  evlsval  21206  evls1fval  21395  fsum2cn  23940  iunmbl2  24626  dvfsumlem1  25095  itgsubst  25118  q1pval  25223  r1pval  25226  rlimcnp2  26021  fsumdvdscom  26239  fsumdvdsmul  26249  ttgval  27140  fsumiunle  31045  msrfval  33399  poimirlem1  35705  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  cdleme31snd  38327  cdlemeg46c  38454  cdlemkid2  38865  cdlemk46  38889  cdlemk53b  38897  cdlemk53  38898  monotuz  40679  oddcomabszz  40682  fnwe2val  40790  fnwe2lem1  40791  fnwe2lem2  40792  mendval  40924  sumsnd  42458  climinf2mpt  43145  climinfmpt  43146  sge0f1o  43810  rnghmval  45337  dmmpossx2  45560