Theorem csbeq1d 3889

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

Syntax hints:   → wi 4   = wceq 1533  ⦋csb 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-sbc 3770  df-csb 3886

This theorem is referenced by:  csbeq12dv  3894  csbco3g  4420  csbidm  4422  fmptcof  7120  mpomptsx  8043  dmmpossx  8045  fmpox  8046  ovmptss  8073  fmpoco  8075  xpf1o  9134  hsmexlem2  10417  iundom2g  10530  sumeq2ii  15635  summolem3  15656  summolem2a  15657  summo  15659  zsum  15660  fsum  15662  sumsnf  15685  fsumcnv  15715  fsumcom2  15716  fsumshftm  15723  fsum0diag2  15725  prodeq2ii  15853  prodmolem3  15873  prodmolem2a  15874  prodmo  15876  zprod  15877  fprod  15881  prodsn  15902  prodsnf  15904  fprodcnv  15923  fprodcom2  15924  bpolylem  15988  bpolyval  15989  ruclem1  16170  pcmpt  16821  gsumvalx  18596  odfval  19437  odfvalALT  19438  odval  19439  telgsumfzslem  19893  telgsumfzs  19894  rnghmval  20327  psrval  21768  psrass1lemOLD  21793  psrass1lem  21796  mpfrcl  21949  evlsval  21950  evls1fval  22148  fsum2cn  24699  iunmbl2  25396  dvfsumlem1  25870  itgsubst  25894  q1pval  25999  r1pval  26002  rlimcnp2  26802  fsumdvdscom  27021  fsumdvdsmul  27031  fsumdvdsmulOLD  27033  mulsval  27913  precsexlemcbv  28008  precsexlem3  28011  ttgvalOLD  28551  fsumiunle  32459  msrfval  34983  poimirlem1  36945  poimirlem3  36947  poimirlem4  36948  poimirlem5  36949  poimirlem6  36950  poimirlem7  36951  poimirlem8  36952  poimirlem10  36954  poimirlem11  36955  poimirlem12  36956  poimirlem15  36959  poimirlem16  36960  poimirlem17  36961  poimirlem18  36962  poimirlem19  36963  poimirlem20  36964  poimirlem21  36965  poimirlem22  36966  poimirlem23  36967  poimirlem24  36968  poimirlem25  36969  poimirlem26  36970  poimirlem27  36971  poimirlem28  36972  cdleme31snd  39713  cdlemeg46c  39840  cdlemkid2  40251  cdlemk46  40275  cdlemk53b  40283  cdlemk53  40284  fmpocos  41515  monotuz  42135  oddcomabszz  42138  fnwe2val  42246  fnwe2lem1  42247  fnwe2lem2  42248  mendval  42380  sumsnd  44165  climinf2mpt  44881  climinfmpt  44882  sge0f1o  45549  dmmpossx2  47167