Theorem csbeq1d 3869

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

Syntax hints:   → wi 4   = wceq 1540  ⦋csb 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3757  df-csb 3866

This theorem is referenced by:  csbeq12dv  3874  csbco3g  4397  csbidm  4399  fmptcof  7105  mpomptsx  8046  dmmpossx  8048  fmpox  8049  ovmptss  8075  fmpoco  8077  xpf1o  9109  hsmexlem2  10387  iundom2g  10500  sumeq2ii  15666  summolem3  15687  summolem2a  15688  summo  15690  zsum  15691  fsum  15693  sumsnf  15716  fsumcnv  15746  fsumcom2  15747  fsumshftm  15754  fsum0diag2  15756  prodeq2ii  15884  prodmolem3  15906  prodmolem2a  15907  prodmo  15909  zprod  15910  fprod  15914  prodsn  15935  prodsnf  15937  fprodcnv  15956  fprodcom2  15957  bpolylem  16021  bpolyval  16022  ruclem1  16206  pcmpt  16870  gsumvalx  18610  odfval  19469  odfvalALT  19470  odval  19471  telgsumfzslem  19925  telgsumfzs  19926  rnghmval  20356  psrval  21831  psrass1lem  21848  mpfrcl  21999  evlsval  22000  evls1fval  22213  fsum2cn  24769  iunmbl2  25465  dvfsumlem1  25939  itgsubst  25963  q1pval  26067  r1pval  26070  rlimcnp2  26883  fsumdvdscom  27102  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  mulsval  28019  precsexlemcbv  28115  precsexlem3  28118  fsumiunle  32761  msrfval  35531  weiunlem1  36457  weiunpo  36460  weiunso  36461  weiunfr  36462  weiunse  36463  poimirlem1  37622  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  cdleme31snd  40387  cdlemeg46c  40514  cdlemkid2  40925  cdlemk46  40949  cdlemk53b  40957  cdlemk53  40958  deg1gprod  42135  fmpocos  42229  monotuz  42937  oddcomabszz  42940  fnwe2val  43045  fnwe2lem1  43046  fnwe2lem2  43047  mendval  43175  sumsnd  45027  climinf2mpt  45719  climinfmpt  45720  sge0f1o  46387  grtri  47943  dmmpossx2  48329  dfswapf2  49254