Theorem csbeq1d 3878

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

Syntax hints:   → wi 4   = wceq 1540  ⦋csb 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766  df-csb 3875

This theorem is referenced by:  csbeq12dv  3883  csbco3g  4406  csbidm  4408  fmptcof  7119  mpomptsx  8061  dmmpossx  8063  fmpox  8064  ovmptss  8090  fmpoco  8092  xpf1o  9151  hsmexlem2  10439  iundom2g  10552  sumeq2ii  15707  summolem3  15728  summolem2a  15729  summo  15731  zsum  15732  fsum  15734  sumsnf  15757  fsumcnv  15787  fsumcom2  15788  fsumshftm  15795  fsum0diag2  15797  prodeq2ii  15925  prodmolem3  15947  prodmolem2a  15948  prodmo  15950  zprod  15951  fprod  15955  prodsn  15976  prodsnf  15978  fprodcnv  15997  fprodcom2  15998  bpolylem  16062  bpolyval  16063  ruclem1  16247  pcmpt  16910  gsumvalx  18652  odfval  19511  odfvalALT  19512  odval  19513  telgsumfzslem  19967  telgsumfzs  19968  rnghmval  20398  psrval  21873  psrass1lem  21890  mpfrcl  22041  evlsval  22042  evls1fval  22255  fsum2cn  24811  iunmbl2  25508  dvfsumlem1  25982  itgsubst  26006  q1pval  26110  r1pval  26113  rlimcnp2  26926  fsumdvdscom  27145  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  mulsval  28052  precsexlemcbv  28147  precsexlem3  28150  fsumiunle  32754  msrfval  35505  weiunlem1  36426  weiunpo  36429  weiunso  36430  weiunfr  36431  weiunse  36432  poimirlem1  37591  poimirlem3  37593  poimirlem4  37594  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  cdleme31snd  40351  cdlemeg46c  40478  cdlemkid2  40889  cdlemk46  40913  cdlemk53b  40921  cdlemk53  40922  deg1gprod  42099  fmpocos  42232  monotuz  42912  oddcomabszz  42915  fnwe2val  43020  fnwe2lem1  43021  fnwe2lem2  43022  mendval  43150  sumsnd  44998  climinf2mpt  45691  climinfmpt  45692  sge0f1o  46359  grtri  47900  dmmpossx2  48260  dfswapf2  49126