Theorem csbeq1d 3889

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

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

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 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-sbc 3770  df-csb 3886

This theorem is referenced by:  csbeq12dv  3894  csbco3g  4420  csbidm  4422  fmptcof  7120  mpomptsx  8043  dmmpossx  8045  fmpox  8046  ovmptss  8073  fmpoco  8075  xpf1o  9135  hsmexlem2  10418  iundom2g  10531  sumeq2ii  15636  summolem3  15657  summolem2a  15658  summo  15660  zsum  15661  fsum  15663  sumsnf  15686  fsumcnv  15716  fsumcom2  15717  fsumshftm  15724  fsum0diag2  15726  prodeq2ii  15854  prodmolem3  15874  prodmolem2a  15875  prodmo  15877  zprod  15878  fprod  15882  prodsn  15903  prodsnf  15905  fprodcnv  15924  fprodcom2  15925  bpolylem  15989  bpolyval  15990  ruclem1  16171  pcmpt  16824  gsumvalx  18599  odfval  19442  odfvalALT  19443  odval  19444  telgsumfzslem  19898  telgsumfzs  19899  rnghmval  20332  psrval  21777  psrass1lemOLD  21802  psrass1lem  21805  mpfrcl  21958  evlsval  21959  evls1fval  22160  fsum2cn  24711  iunmbl2  25408  dvfsumlem1  25882  itgsubst  25906  q1pval  26011  r1pval  26014  rlimcnp2  26814  fsumdvdscom  27033  fsumdvdsmul  27043  fsumdvdsmulOLD  27045  mulsval  27925  precsexlemcbv  28020  precsexlem3  28023  ttgvalOLD  28596  fsumiunle  32502  msrfval  35017  poimirlem1  36979  poimirlem3  36981  poimirlem4  36982  poimirlem5  36983  poimirlem6  36984  poimirlem7  36985  poimirlem8  36986  poimirlem10  36988  poimirlem11  36989  poimirlem12  36990  poimirlem15  36993  poimirlem16  36994  poimirlem17  36995  poimirlem18  36996  poimirlem19  36997  poimirlem20  36998  poimirlem21  36999  poimirlem22  37000  poimirlem23  37001  poimirlem24  37002  poimirlem25  37003  poimirlem26  37004  poimirlem27  37005  poimirlem28  37006  cdleme31snd  39747  cdlemeg46c  39874  cdlemkid2  40285  cdlemk46  40309  cdlemk53b  40317  cdlemk53  40318  fmpocos  41549  monotuz  42169  oddcomabszz  42172  fnwe2val  42280  fnwe2lem1  42281  fnwe2lem2  42282  mendval  42414  sumsnd  44199  climinf2mpt  44915  climinfmpt  44916  sge0f1o  45583  dmmpossx2  47201