Theorem csbeq1d 3842

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

Syntax hints:   → wi 4   = wceq 1542  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbeq12dv  3847  csbco3g  4372  csbidm  4374  fmptcof  7085  mpomptsx  8019  dmmpossx  8021  fmpox  8022  ovmptss  8045  fmpoco  8047  xpf1o  9079  hsmexlem2  10351  iundom2g  10464  sumeq2ii  15657  summolem3  15678  summolem2a  15679  summo  15681  zsum  15682  fsum  15684  sumsnf  15707  fsumcnv  15737  fsumcom2  15738  fsumshftm  15745  fsum0diag2  15747  prodeq2ii  15878  prodmolem3  15900  prodmolem2a  15901  prodmo  15903  zprod  15904  fprod  15908  prodsn  15929  prodsnf  15931  fprodcnv  15950  fprodcom2  15951  bpolylem  16015  bpolyval  16016  ruclem1  16200  pcmpt  16865  gsumvalx  18646  odfval  19509  odfvalALT  19510  odval  19511  telgsumfzslem  19965  telgsumfzs  19966  rnghmval  20422  psrval  21897  psrass1lem  21914  mpfrcl  22065  evlsval  22066  evls1fval  22286  fsum2cn  24840  iunmbl2  25526  dvfsumlem1  25995  itgsubst  26018  q1pval  26122  r1pval  26125  rlimcnp2  26932  fsumdvdscom  27150  fsumdvdsmul  27160  mulsval  28103  precsexlemcbv  28200  precsexlem3  28203  fsumiunle  32904  msrfval  35721  weiunval  36646  weiunpo  36649  weiunso  36650  weiunfr  36651  weiunse  36652  poimirlem1  37944  poimirlem3  37946  poimirlem4  37947  poimirlem5  37948  poimirlem6  37949  poimirlem7  37950  poimirlem8  37951  poimirlem10  37953  poimirlem11  37954  poimirlem12  37955  poimirlem15  37958  poimirlem16  37959  poimirlem17  37960  poimirlem18  37961  poimirlem19  37962  poimirlem20  37963  poimirlem21  37964  poimirlem22  37965  poimirlem23  37966  poimirlem24  37967  poimirlem25  37968  poimirlem26  37969  poimirlem27  37970  poimirlem28  37971  cdleme31snd  40834  cdlemeg46c  40961  cdlemkid2  41372  cdlemk46  41396  cdlemk53b  41404  cdlemk53  41405  deg1gprod  42581  fmpocos  42677  monotuz  43371  oddcomabszz  43374  fnwe2val  43479  fnwe2lem1  43480  fnwe2lem2  43481  mendval  43609  sumsnd  45459  climinf2mpt  46144  climinfmpt  46145  sge0f1o  46812  grtri  48418  dmmpossx2  48815  dfswapf2  49738