Theorem csbeq1d 3903

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789  df-csb 3900

This theorem is referenced by:  csbeq12dv  3908  csbco3g  4431  csbidm  4433  fmptcof  7150  mpomptsx  8089  dmmpossx  8091  fmpox  8092  ovmptss  8118  fmpoco  8120  xpf1o  9179  hsmexlem2  10467  iundom2g  10580  sumeq2ii  15729  summolem3  15750  summolem2a  15751  summo  15753  zsum  15754  fsum  15756  sumsnf  15779  fsumcnv  15809  fsumcom2  15810  fsumshftm  15817  fsum0diag2  15819  prodeq2ii  15947  prodmolem3  15969  prodmolem2a  15970  prodmo  15972  zprod  15973  fprod  15977  prodsn  15998  prodsnf  16000  fprodcnv  16019  fprodcom2  16020  bpolylem  16084  bpolyval  16085  ruclem1  16267  pcmpt  16930  gsumvalx  18689  odfval  19550  odfvalALT  19551  odval  19552  telgsumfzslem  20006  telgsumfzs  20007  rnghmval  20440  psrval  21935  psrass1lem  21952  mpfrcl  22109  evlsval  22110  evls1fval  22323  fsum2cn  24895  iunmbl2  25592  dvfsumlem1  26066  itgsubst  26090  q1pval  26194  r1pval  26197  rlimcnp2  27009  fsumdvdscom  27228  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  mulsval  28135  precsexlemcbv  28230  precsexlem3  28233  ttgvalOLD  28884  fsumiunle  32831  msrfval  35542  weiunlem1  36463  weiunpo  36466  weiunso  36467  weiunfr  36468  weiunse  36469  poimirlem1  37628  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  cdleme31snd  40388  cdlemeg46c  40515  cdlemkid2  40926  cdlemk46  40950  cdlemk53b  40958  cdlemk53  40959  deg1gprod  42141  fmpocos  42275  monotuz  42953  oddcomabszz  42956  fnwe2val  43061  fnwe2lem1  43062  fnwe2lem2  43063  mendval  43191  sumsnd  45031  climinf2mpt  45729  climinfmpt  45730  sge0f1o  46397  grtri  47907  dmmpossx2  48253  dfswapf2  48967