Theorem csbeq1d 3836

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

Syntax hints:   → wi 4   = wceq 1539  ⦋csb 3832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sbc 3717  df-csb 3833

This theorem is referenced by:  csbeq12dv  3841  csbco3g  4362  csbidm  4364  fmptcof  7002  mpomptsx  7904  dmmpossx  7906  fmpox  7907  ovmptss  7933  fmpoco  7935  xpf1o  8926  hsmexlem2  10183  iundom2g  10296  sumeq2ii  15405  summolem3  15426  summolem2a  15427  summo  15429  zsum  15430  fsum  15432  sumsnf  15455  fsumcnv  15485  fsumcom2  15486  fsumshftm  15493  fsum0diag2  15495  prodeq2ii  15623  prodmolem3  15643  prodmolem2a  15644  prodmo  15646  zprod  15647  fprod  15651  prodsn  15672  prodsnf  15674  fprodcnv  15693  fprodcom2  15694  bpolylem  15758  bpolyval  15759  ruclem1  15940  pcmpt  16593  gsumvalx  18360  odfval  19140  odfvalALT  19141  odval  19142  telgsumfzslem  19589  telgsumfzs  19590  psrval  21118  psrass1lemOLD  21143  psrass1lem  21146  mpfrcl  21295  evlsval  21296  evls1fval  21485  fsum2cn  24034  iunmbl2  24721  dvfsumlem1  25190  itgsubst  25213  q1pval  25318  r1pval  25321  rlimcnp2  26116  fsumdvdscom  26334  fsumdvdsmul  26344  ttgvalOLD  27237  fsumiunle  31143  msrfval  33499  poimirlem1  35778  poimirlem3  35780  poimirlem4  35781  poimirlem5  35782  poimirlem6  35783  poimirlem7  35784  poimirlem8  35785  poimirlem10  35787  poimirlem11  35788  poimirlem12  35789  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem18  35795  poimirlem19  35796  poimirlem20  35797  poimirlem21  35798  poimirlem22  35799  poimirlem23  35800  poimirlem24  35801  poimirlem25  35802  poimirlem26  35803  poimirlem27  35804  poimirlem28  35805  cdleme31snd  38400  cdlemeg46c  38527  cdlemkid2  38938  cdlemk46  38962  cdlemk53b  38970  cdlemk53  38971  monotuz  40763  oddcomabszz  40766  fnwe2val  40874  fnwe2lem1  40875  fnwe2lem2  40876  mendval  41008  sumsnd  42569  climinf2mpt  43255  climinfmpt  43256  sge0f1o  43920  rnghmval  45449  dmmpossx2  45672