Theorem csbeq1d 3842

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

Syntax hints:   → wi 4   = wceq 1542  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbeq12dv  3847  csbco3g  4372  csbidm  4374  fmptcof  7075  mpomptsx  8008  dmmpossx  8010  fmpox  8011  ovmptss  8034  fmpoco  8036  xpf1o  9068  hsmexlem2  10338  iundom2g  10451  sumeq2ii  15617  summolem3  15638  summolem2a  15639  summo  15641  zsum  15642  fsum  15644  sumsnf  15667  fsumcnv  15697  fsumcom2  15698  fsumshftm  15705  fsum0diag2  15707  prodeq2ii  15835  prodmolem3  15857  prodmolem2a  15858  prodmo  15860  zprod  15861  fprod  15865  prodsn  15886  prodsnf  15888  fprodcnv  15907  fprodcom2  15908  bpolylem  15972  bpolyval  15973  ruclem1  16157  pcmpt  16821  gsumvalx  18602  odfval  19465  odfvalALT  19466  odval  19467  telgsumfzslem  19921  telgsumfzs  19922  rnghmval  20378  psrval  21872  psrass1lem  21889  mpfrcl  22041  evlsval  22042  evls1fval  22262  fsum2cn  24816  iunmbl2  25502  dvfsumlem1  25973  itgsubst  25997  q1pval  26101  r1pval  26104  rlimcnp2  26916  fsumdvdscom  27135  fsumdvdsmul  27145  fsumdvdsmulOLD  27147  mulsval  28089  precsexlemcbv  28186  precsexlem3  28189  fsumiunle  32893  msrfval  35725  weiunval  36650  weiunpo  36653  weiunso  36654  weiunfr  36655  weiunse  36656  poimirlem1  37933  poimirlem3  37935  poimirlem4  37936  poimirlem5  37937  poimirlem6  37938  poimirlem7  37939  poimirlem8  37940  poimirlem10  37942  poimirlem11  37943  poimirlem12  37944  poimirlem15  37947  poimirlem16  37948  poimirlem17  37949  poimirlem18  37950  poimirlem19  37951  poimirlem20  37952  poimirlem21  37953  poimirlem22  37954  poimirlem23  37955  poimirlem24  37956  poimirlem25  37957  poimirlem26  37958  poimirlem27  37959  poimirlem28  37960  cdleme31snd  40823  cdlemeg46c  40950  cdlemkid2  41361  cdlemk46  41385  cdlemk53b  41393  cdlemk53  41394  deg1gprod  42571  fmpocos  42667  monotuz  43372  oddcomabszz  43375  fnwe2val  43480  fnwe2lem1  43481  fnwe2lem2  43482  mendval  43610  sumsnd  45460  climinf2mpt  46146  climinfmpt  46147  sge0f1o  46814  grtri  48374  dmmpossx2  48771  dfswapf2  49694