Theorem csbeq1d 3856

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⦋csb 3852

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3744  df-csb 3853

This theorem is used by:  csbeq12dv  3861  csbco3g  4395  csbidm  4397  fmptcof  7126  mpomptsx  8059  dmmpossx  8061  fmpox  8062  ovmptss  8086  fmpoco  8088  xpf1o  9125  hsmexlem2  10417  iundom2g  10530  sumeq2ii  15751  summolem3  15772  summolem2a  15773  summo  15775  zsum  15776  fsum  15778  sumsnf  15801  fsumcnv  15831  fsumcom2  15832  fsumshftm  15839  fsum0diag2  15841  prodeq2ii  15972  prodmolem3  15994  prodmolem2a  15995  prodmo  15997  zprod  15998  fprod  16002  prodsn  16023  prodsnf  16025  fprodcnv  16044  fprodcom2  16045  bpolylem  16108  bpolyval  16109  ruclem1  16293  pcmpt  16958  gsumvalx  18740  odfval  19608  odfvalALT  19609  odval  19610  telgsumfzslem  20064  telgsumfzs  20065  rnghmval  20529  rhmval0  20564  psrval  22076  psrass1lem  22094  mpfrcl  22247  evlsval  22248  evls1fval  22490  fsum2cn  25041  iunmbl2  25727  dvfsumlem1  26196  itgsubst  26219  q1pval  26323  r1pval  26326  rlimcnp2  27142  fsumdvdscom  27360  fsumdvdsmul  27370  mulsval  28313  precsexlemcbv  28410  precsexlem3  28413  fsumiunle  33184  msrfval  36037  nmulprop  36690  weiunval  37001  weiunpo  37004  weiunso  37005  weiunfr  37006  weiunse  37007  poimirlem1  38300  poimirlem3  38302  poimirlem4  38303  poimirlem5  38304  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem23  38322  poimirlem24  38323  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem28  38327  cdleme31snd  41188  cdlemeg46c  41315  cdlemkid2  41726  cdlemk46  41750  cdlemk53b  41758  cdlemk53  41759  deg1gprod  42935  fmpocos  43032  monotuz  43696  oddcomabszz  43699  fnwe2val  43804  fnwe2lem1  43805  fnwe2lem2  43806  mendval  43934  sumsnd  45774  climinf2mpt  46456  climinfmpt  46457  sge0f1o  47124  grtri  48733  dmmpossx2  49145  dfswapf2  50067