Theorem csbeq1d 3646

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

Syntax hints:   → wi 4   = wceq 1596  ⦋csb 3639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-sbc 3542  df-csb 3640

This theorem is referenced by:  csbco3g  4108  csbidm  4110  fmptcof  6512  mpt2mptsx  7353  dmmpt2ssx  7355  fmpt2x  7356  ovmptss  7378  fmpt2co  7380  xpf1o  8238  hsmexlem2  9362  iundom2g  9475  sumeq2ii  14543  summolem3  14565  summolem2a  14566  summo  14568  zsum  14569  fsum  14571  sumsnf  14593  sumsn  14595  fsumcnv  14624  fsumcom2  14625  fsumcom2OLD  14626  fsumshftm  14633  fsum0diag2  14635  prodeq2ii  14763  prodmolem3  14783  prodmolem2a  14784  prodmo  14786  zprod  14787  fprod  14791  prodsn  14812  prodsnf  14814  fprodcnv  14833  fprodcom2  14834  fprodcom2OLD  14835  bpolylem  14899  bpolyval  14900  ruclem1  15080  pcmpt  15719  gsumvalx  17392  odfval  18073  odval  18074  telgsumfzslem  18506  telgsumfzs  18507  psrval  19485  psrass1lem  19500  mpfrcl  19641  evlsval  19642  evls1fval  19807  fsum2cn  22796  iunmbl2  23446  dvfsumlem1  23909  itgsubst  23932  q1pval  24033  r1pval  24036  rlimcnp2  24813  fsumdvdscom  25031  fsumdvdsmul  25041  ttgval  25875  fsumiunle  29805  msrfval  31662  poimirlem1  33642  poimirlem3  33644  poimirlem4  33645  poimirlem5  33646  poimirlem6  33647  poimirlem7  33648  poimirlem8  33649  poimirlem10  33651  poimirlem11  33652  poimirlem12  33653  poimirlem15  33656  poimirlem16  33657  poimirlem17  33658  poimirlem18  33659  poimirlem19  33660  poimirlem20  33661  poimirlem21  33662  poimirlem22  33663  poimirlem23  33664  poimirlem24  33665  poimirlem25  33666  poimirlem26  33667  poimirlem27  33668  poimirlem28  33669  cdleme31snd  36093  cdlemeg46c  36220  cdlemkid2  36631  cdlemk46  36655  cdlemk53b  36663  cdlemk53  36664  monotuz  37925  oddcomabszz  37928  fnwe2val  38038  fnwe2lem1  38039  fnwe2lem2  38040  mendval  38172  sumsnd  39601  climinf2mpt  40366  climinfmpt  40367  sge0f1o  41019  rnghmval  42318  dmmpt2ssx2  42542