Theorem csbeq1d 3854

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

Syntax hints:   → wi 4   = wceq 1542  ⦋csb 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3742  df-csb 3851

This theorem is referenced by:  csbeq12dv  3859  csbco3g  4384  csbidm  4386  fmptcof  7077  mpomptsx  8010  dmmpossx  8012  fmpox  8013  ovmptss  8037  fmpoco  8039  xpf1o  9071  hsmexlem2  10341  iundom2g  10454  sumeq2ii  15620  summolem3  15641  summolem2a  15642  summo  15644  zsum  15645  fsum  15647  sumsnf  15670  fsumcnv  15700  fsumcom2  15701  fsumshftm  15708  fsum0diag2  15710  prodeq2ii  15838  prodmolem3  15860  prodmolem2a  15861  prodmo  15863  zprod  15864  fprod  15868  prodsn  15889  prodsnf  15891  fprodcnv  15910  fprodcom2  15911  bpolylem  15975  bpolyval  15976  ruclem1  16160  pcmpt  16824  gsumvalx  18605  odfval  19465  odfvalALT  19466  odval  19467  telgsumfzslem  19921  telgsumfzs  19922  rnghmval  20380  psrval  21875  psrass1lem  21892  mpfrcl  22044  evlsval  22045  evls1fval  22267  fsum2cn  24822  iunmbl2  25518  dvfsumlem1  25992  itgsubst  26016  q1pval  26120  r1pval  26123  rlimcnp2  26936  fsumdvdscom  27155  fsumdvdsmul  27165  fsumdvdsmulOLD  27167  mulsval  28091  precsexlemcbv  28187  precsexlem3  28190  fsumiunle  32891  msrfval  35712  weiunlem1  36637  weiunpo  36640  weiunso  36641  weiunfr  36642  weiunse  36643  poimirlem1  37793  poimirlem3  37795  poimirlem4  37796  poimirlem5  37797  poimirlem6  37798  poimirlem7  37799  poimirlem8  37800  poimirlem10  37802  poimirlem11  37803  poimirlem12  37804  poimirlem15  37807  poimirlem16  37808  poimirlem17  37809  poimirlem18  37810  poimirlem19  37811  poimirlem20  37812  poimirlem21  37813  poimirlem22  37814  poimirlem23  37815  poimirlem24  37816  poimirlem25  37817  poimirlem26  37818  poimirlem27  37819  poimirlem28  37820  cdleme31snd  40683  cdlemeg46c  40810  cdlemkid2  41221  cdlemk46  41245  cdlemk53b  41253  cdlemk53  41254  deg1gprod  42431  fmpocos  42527  monotuz  43219  oddcomabszz  43222  fnwe2val  43327  fnwe2lem1  43328  fnwe2lem2  43329  mendval  43457  sumsnd  45307  climinf2mpt  45994  climinfmpt  45995  sge0f1o  46662  grtri  48222  dmmpossx2  48619  dfswapf2  49542