Theorem csbeq1d 3855

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⦋csb 3851

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sbc 3743  df-csb 3852

This theorem is used by:  csbeq12dv  3860  csbco3g  4392  csbidm  4394  fmptcof  7155  mpomptsx  8100  dmmpossx  8102  fmpox  8103  ovmptssOLD  8130  fmpoco  8132  fnwe2lem1  8172  fnwe2lem2  8173  fnwe2lem3  8174  xpf1o  9186  hsmexlem2  10532  iundom2g  10651  sumeq2ii  15889  summolem3  15909  summolem2a  15910  summo  15912  zsum  15913  fsum  15915  sumsnf  15938  fsumcnv  15968  fsumcom2  15969  fsumshftm  15976  fsum0diag2  15978  prodeq2ii  16109  prodmolem3  16129  prodmolem2a  16130  prodmo  16132  zprod  16133  fprod  16137  prodsn  16158  prodsnf  16160  fprodcnv  16179  fprodcom2  16180  bpolylem  16243  bpolyval  16244  ruclem1  16428  pcmpt  17099  gsumvalx  18894  odfval  19776  odfvalALT  19777  odval  19778  telgsumfzslem  20232  telgsumfzs  20233  rnghmval  20700  rhmval0  20735  psrval  22253  psrass1lem  22271  mpfrcl  22424  evlsval  22425  evls1fval  22667  fsum2cn  25222  iunmbl2  25908  dvfsumlem1  26376  itgsubst  26399  q1pval  26503  r1pval  26506  rlimcnp2  27324  fsumdvdscom  27542  fsumdvdsmul  27552  mulsval  28525  precsexlemcbv  28622  precsexlem3  28625  fsumiunle  33490  msrfval  36469  nmulprop  37117  weiunval  37428  weiunpo  37431  weiunso  37432  weiunfr  37433  weiunse  37434  poimirlem1  38731  poimirlem3  38733  poimirlem4  38734  poimirlem5  38735  poimirlem6  38736  poimirlem7  38737  poimirlem8  38738  poimirlem10  38740  poimirlem11  38741  poimirlem12  38742  poimirlem15  38745  poimirlem16  38746  poimirlem17  38747  poimirlem18  38748  poimirlem19  38749  poimirlem20  38750  poimirlem21  38751  poimirlem22  38752  poimirlem23  38753  poimirlem24  38754  poimirlem25  38755  poimirlem26  38756  poimirlem27  38757  poimirlem28  38758  cdleme31snd  41635  cdlemeg46c  41762  cdlemkid2  42173  cdlemk46  42197  cdlemk53b  42205  cdlemk53  42206  deg1gprod  43382  fmpocos  43480  monotuz  44141  oddcomabszz  44144  mendval  44373  sumsnd  46248  climinf2mpt  46929  climinfmpt  46930  sge0f1o  47597  grtri  49243  dmmpossx2  49654  dfswapf2  50588