Theorem csbeq1d 3854

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

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

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 3742  df-csb 3851

This theorem is referenced by:  csbeq12dv  3859  csbco3g  4384  csbidm  4386  fmptcof  7078  mpomptsx  8011  dmmpossx  8013  fmpox  8014  ovmptss  8038  fmpoco  8040  xpf1o  9072  hsmexlem2  10342  iundom2g  10455  sumeq2ii  15621  summolem3  15642  summolem2a  15643  summo  15645  zsum  15646  fsum  15648  sumsnf  15671  fsumcnv  15701  fsumcom2  15702  fsumshftm  15709  fsum0diag2  15711  prodeq2ii  15839  prodmolem3  15861  prodmolem2a  15862  prodmo  15864  zprod  15865  fprod  15869  prodsn  15890  prodsnf  15892  fprodcnv  15911  fprodcom2  15912  bpolylem  15976  bpolyval  15977  ruclem1  16161  pcmpt  16825  gsumvalx  18606  odfval  19466  odfvalALT  19467  odval  19468  telgsumfzslem  19922  telgsumfzs  19923  rnghmval  20381  psrval  21876  psrass1lem  21893  mpfrcl  22045  evlsval  22046  evls1fval  22268  fsum2cn  24823  iunmbl2  25519  dvfsumlem1  25993  itgsubst  26017  q1pval  26121  r1pval  26124  rlimcnp2  26937  fsumdvdscom  27156  fsumdvdsmul  27166  fsumdvdsmulOLD  27168  mulsval  28110  precsexlemcbv  28207  precsexlem3  28210  fsumiunle  32913  msrfval  35744  weiunval  36669  weiunpo  36672  weiunso  36673  weiunfr  36674  weiunse  36675  poimirlem1  37835  poimirlem3  37837  poimirlem4  37838  poimirlem5  37839  poimirlem6  37840  poimirlem7  37841  poimirlem8  37842  poimirlem10  37844  poimirlem11  37845  poimirlem12  37846  poimirlem15  37849  poimirlem16  37850  poimirlem17  37851  poimirlem18  37852  poimirlem19  37853  poimirlem20  37854  poimirlem21  37855  poimirlem22  37856  poimirlem23  37857  poimirlem24  37858  poimirlem25  37859  poimirlem26  37860  poimirlem27  37861  poimirlem28  37862  cdleme31snd  40725  cdlemeg46c  40852  cdlemkid2  41263  cdlemk46  41287  cdlemk53b  41295  cdlemk53  41296  deg1gprod  42473  fmpocos  42569  monotuz  43261  oddcomabszz  43264  fnwe2val  43369  fnwe2lem1  43370  fnwe2lem2  43371  mendval  43499  sumsnd  45349  climinf2mpt  46035  climinfmpt  46036  sge0f1o  46703  grtri  48263  dmmpossx2  48660  dfswapf2  49583