Theorem csbeq1d 3573

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

Syntax hints:   → wi 4   = wceq 1523  ⦋csb 3566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-sbc 3469  df-csb 3567

This theorem is referenced by:  csbco3g  4033  csbidm  4035  fmptcof  6437  mpt2mptsx  7278  dmmpt2ssx  7280  fmpt2x  7281  ovmptss  7303  fmpt2co  7305  xpf1o  8163  hsmexlem2  9287  iundom2g  9400  sumeq2ii  14467  summolem3  14489  summolem2a  14490  summo  14492  zsum  14493  fsum  14495  sumsnf  14517  sumsn  14519  fsumcnv  14548  fsumcom2  14549  fsumcom2OLD  14550  fsumshftm  14557  fsum0diag2  14559  prodeq2ii  14687  prodmolem3  14707  prodmolem2a  14708  prodmo  14710  zprod  14711  fprod  14715  prodsn  14736  prodsnf  14738  fprodcnv  14757  fprodcom2  14758  fprodcom2OLD  14759  bpolylem  14823  bpolyval  14824  ruclem1  15004  pcmpt  15643  gsumvalx  17317  odfval  17998  odval  17999  telgsumfzslem  18431  telgsumfzs  18432  psrval  19410  psrass1lem  19425  mpfrcl  19566  evlsval  19567  evls1fval  19732  fsum2cn  22721  iunmbl2  23371  dvfsumlem1  23834  itgsubst  23857  q1pval  23958  r1pval  23961  rlimcnp2  24738  fsumdvdscom  24956  fsumdvdsmul  24966  ttgval  25800  fsumiunle  29703  msrfval  31560  poimirlem1  33540  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  cdleme31snd  35991  cdlemeg46c  36118  cdlemkid2  36529  cdlemk46  36553  cdlemk53b  36561  cdlemk53  36562  monotuz  37823  oddcomabszz  37826  fnwe2val  37936  fnwe2lem1  37937  fnwe2lem2  37938  mendval  38070  sumsnd  39499  climinf2mpt  40264  climinfmpt  40265  sge0f1o  40917  rnghmval  42216  dmmpt2ssx2  42440