Theorem csbeq1d 3852

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

Syntax hints:   → wi 4   = wceq 1541  ⦋csb 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3740  df-csb 3849

This theorem is referenced by:  csbeq12dv  3857  csbco3g  4379  csbidm  4381  fmptcof  7058  mpomptsx  7991  dmmpossx  7993  fmpox  7994  ovmptss  8018  fmpoco  8020  xpf1o  9047  hsmexlem2  10310  iundom2g  10423  sumeq2ii  15592  summolem3  15613  summolem2a  15614  summo  15616  zsum  15617  fsum  15619  sumsnf  15642  fsumcnv  15672  fsumcom2  15673  fsumshftm  15680  fsum0diag2  15682  prodeq2ii  15810  prodmolem3  15832  prodmolem2a  15833  prodmo  15835  zprod  15836  fprod  15840  prodsn  15861  prodsnf  15863  fprodcnv  15882  fprodcom2  15883  bpolylem  15947  bpolyval  15948  ruclem1  16132  pcmpt  16796  gsumvalx  18576  odfval  19437  odfvalALT  19438  odval  19439  telgsumfzslem  19893  telgsumfzs  19894  rnghmval  20351  psrval  21845  psrass1lem  21862  mpfrcl  22013  evlsval  22014  evls1fval  22227  fsum2cn  24782  iunmbl2  25478  dvfsumlem1  25952  itgsubst  25976  q1pval  26080  r1pval  26083  rlimcnp2  26896  fsumdvdscom  27115  fsumdvdsmul  27125  fsumdvdsmulOLD  27127  mulsval  28041  precsexlemcbv  28137  precsexlem3  28140  fsumiunle  32802  msrfval  35549  weiunlem1  36475  weiunpo  36478  weiunso  36479  weiunfr  36480  weiunse  36481  poimirlem1  37640  poimirlem3  37642  poimirlem4  37643  poimirlem5  37644  poimirlem6  37645  poimirlem7  37646  poimirlem8  37647  poimirlem10  37649  poimirlem11  37650  poimirlem12  37651  poimirlem15  37654  poimirlem16  37655  poimirlem17  37656  poimirlem18  37657  poimirlem19  37658  poimirlem20  37659  poimirlem21  37660  poimirlem22  37661  poimirlem23  37662  poimirlem24  37663  poimirlem25  37664  poimirlem26  37665  poimirlem27  37666  poimirlem28  37667  cdleme31snd  40404  cdlemeg46c  40531  cdlemkid2  40942  cdlemk46  40966  cdlemk53b  40974  cdlemk53  40975  deg1gprod  42152  fmpocos  42246  monotuz  42953  oddcomabszz  42956  fnwe2val  43061  fnwe2lem1  43062  fnwe2lem2  43063  mendval  43191  sumsnd  45042  climinf2mpt  45731  climinfmpt  45732  sge0f1o  46399  grtri  47950  dmmpossx2  48347  dfswapf2  49272