Theorem csbeq1d 3802

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

Syntax hints:   → wi 4   = wceq 1543  ⦋csb 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-sbc 3684  df-csb 3799

This theorem is referenced by:  csbeq12dv  3807  csbco3g  4329  csbidm  4331  fmptcof  6923  mpomptsx  7812  dmmpossx  7814  fmpox  7815  ovmptss  7839  fmpoco  7841  xpf1o  8786  hsmexlem2  10006  iundom2g  10119  sumeq2ii  15222  summolem3  15243  summolem2a  15244  summo  15246  zsum  15247  fsum  15249  sumsnf  15271  fsumcnv  15300  fsumcom2  15301  fsumshftm  15308  fsum0diag2  15310  prodeq2ii  15438  prodmolem3  15458  prodmolem2a  15459  prodmo  15461  zprod  15462  fprod  15466  prodsn  15487  prodsnf  15489  fprodcnv  15508  fprodcom2  15509  bpolylem  15573  bpolyval  15574  ruclem1  15755  pcmpt  16408  gsumvalx  18102  odfval  18878  odfvalALT  18879  odval  18880  telgsumfzslem  19327  telgsumfzs  19328  psrval  20828  psrass1lemOLD  20853  psrass1lem  20856  mpfrcl  20999  evlsval  21000  evls1fval  21189  fsum2cn  23722  iunmbl2  24408  dvfsumlem1  24877  itgsubst  24900  q1pval  25005  r1pval  25008  rlimcnp2  25803  fsumdvdscom  26021  fsumdvdsmul  26031  ttgval  26920  fsumiunle  30817  msrfval  33166  poimirlem1  35464  poimirlem3  35466  poimirlem4  35467  poimirlem5  35468  poimirlem6  35469  poimirlem7  35470  poimirlem8  35471  poimirlem10  35473  poimirlem11  35474  poimirlem12  35475  poimirlem15  35478  poimirlem16  35479  poimirlem17  35480  poimirlem18  35481  poimirlem19  35482  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem23  35486  poimirlem24  35487  poimirlem25  35488  poimirlem26  35489  poimirlem27  35490  poimirlem28  35491  cdleme31snd  38086  cdlemeg46c  38213  cdlemkid2  38624  cdlemk46  38648  cdlemk53b  38656  cdlemk53  38657  monotuz  40407  oddcomabszz  40410  fnwe2val  40518  fnwe2lem1  40519  fnwe2lem2  40520  mendval  40652  sumsnd  42183  climinf2mpt  42873  climinfmpt  42874  sge0f1o  43538  rnghmval  45065  dmmpossx2  45288