Theorem csbeq1d 3893

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

Syntax hints:   → wi 4   = wceq 1534  ⦋csb 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-sbc 3775  df-csb 3890

This theorem is referenced by:  csbeq12dv  3898  csbco3g  4424  csbidm  4426  fmptcof  7133  mpomptsx  8062  dmmpossx  8064  fmpox  8065  ovmptss  8092  fmpoco  8094  xpf1o  9157  hsmexlem2  10444  iundom2g  10557  sumeq2ii  15665  summolem3  15686  summolem2a  15687  summo  15689  zsum  15690  fsum  15692  sumsnf  15715  fsumcnv  15745  fsumcom2  15746  fsumshftm  15753  fsum0diag2  15755  prodeq2ii  15883  prodmolem3  15903  prodmolem2a  15904  prodmo  15906  zprod  15907  fprod  15911  prodsn  15932  prodsnf  15934  fprodcnv  15953  fprodcom2  15954  bpolylem  16018  bpolyval  16019  ruclem1  16201  pcmpt  16854  gsumvalx  18629  odfval  19480  odfvalALT  19481  odval  19482  telgsumfzslem  19936  telgsumfzs  19937  rnghmval  20372  psrval  21841  psrass1lemOLD  21867  psrass1lem  21870  mpfrcl  22024  evlsval  22025  evls1fval  22231  fsum2cn  24782  iunmbl2  25479  dvfsumlem1  25953  itgsubst  25977  q1pval  26083  r1pval  26086  rlimcnp2  26891  fsumdvdscom  27110  fsumdvdsmul  27120  fsumdvdsmulOLD  27122  mulsval  28002  precsexlemcbv  28097  precsexlem3  28100  ttgvalOLD  28673  fsumiunle  32586  msrfval  35137  poimirlem1  37083  poimirlem3  37085  poimirlem4  37086  poimirlem5  37087  poimirlem6  37088  poimirlem7  37089  poimirlem8  37090  poimirlem10  37092  poimirlem11  37093  poimirlem12  37094  poimirlem15  37097  poimirlem16  37098  poimirlem17  37099  poimirlem18  37100  poimirlem19  37101  poimirlem20  37102  poimirlem21  37103  poimirlem22  37104  poimirlem23  37105  poimirlem24  37106  poimirlem25  37107  poimirlem26  37108  poimirlem27  37109  poimirlem28  37110  cdleme31snd  39848  cdlemeg46c  39975  cdlemkid2  40386  cdlemk46  40410  cdlemk53b  40418  cdlemk53  40419  deg1gprod  41596  fmpocos  41697  monotuz  42334  oddcomabszz  42337  fnwe2val  42445  fnwe2lem1  42446  fnwe2lem2  42447  mendval  42579  sumsnd  44360  climinf2mpt  45074  climinfmpt  45075  sge0f1o  45742  dmmpossx2  47372