Theorem csbeq1d 3850

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbeq12dv  3855  csbco3g  4388  csbidm  4390  fmptcof  7131  mpomptsx  8075  dmmpossx  8077  fmpox  8078  ovmptss  8104  fmpoco  8106  fnwe2lem1  8145  fnwe2lem2  8146  fnwe2lem3  8147  xpf1o  9158  hsmexlem2  10505  iundom2g  10624  sumeq2ii  15860  summolem3  15880  summolem2a  15881  summo  15883  zsum  15884  fsum  15886  sumsnf  15909  fsumcnv  15939  fsumcom2  15940  fsumshftm  15947  fsum0diag2  15949  prodeq2ii  16080  prodmolem3  16100  prodmolem2a  16101  prodmo  16103  zprod  16104  fprod  16108  prodsn  16129  prodsnf  16131  fprodcnv  16150  fprodcom2  16151  bpolylem  16214  bpolyval  16215  ruclem1  16399  pcmpt  17070  gsumvalx  18865  odfval  19746  odfvalALT  19747  odval  19748  telgsumfzslem  20202  telgsumfzs  20203  rnghmval  20670  rhmval0  20705  psrval  22223  psrass1lem  22241  mpfrcl  22394  evlsval  22395  evls1fval  22637  fsum2cn  25192  iunmbl2  25878  dvfsumlem1  26346  itgsubst  26369  q1pval  26473  r1pval  26476  rlimcnp2  27294  fsumdvdscom  27512  fsumdvdsmul  27522  mulsval  28495  precsexlemcbv  28592  precsexlem3  28595  fsumiunle  33462  msrfval  36344  nmulprop  36981  weiunval  37292  weiunpo  37295  weiunso  37296  weiunfr  37297  weiunse  37298  poimirlem1  38582  poimirlem3  38584  poimirlem4  38585  poimirlem5  38586  poimirlem6  38587  poimirlem7  38588  poimirlem8  38589  poimirlem10  38591  poimirlem11  38592  poimirlem12  38593  poimirlem15  38596  poimirlem16  38597  poimirlem17  38598  poimirlem18  38599  poimirlem19  38600  poimirlem20  38601  poimirlem21  38602  poimirlem22  38603  poimirlem23  38604  poimirlem24  38605  poimirlem25  38606  poimirlem26  38607  poimirlem27  38608  poimirlem28  38609  cdleme31snd  41486  cdlemeg46c  41613  cdlemkid2  42024  cdlemk46  42048  cdlemk53b  42056  cdlemk53  42057  deg1gprod  43233  fmpocos  43330  monotuz  43991  oddcomabszz  43994  mendval  44224  sumsnd  46086  climinf2mpt  46767  climinfmpt  46768  sge0f1o  47435  grtri  49081  dmmpossx2  49492  dfswapf2  50412