Theorem csbeq1d 3886

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3772  df-csb 3883

This theorem is referenced by:  csbeq12dv  3891  csbco3g  4379  csbidm  4381  fmptcof  6886  mpomptsx  7756  dmmpossx  7758  fmpox  7759  ovmptss  7782  fmpoco  7784  xpf1o  8673  hsmexlem2  9843  iundom2g  9956  sumeq2ii  15044  summolem3  15065  summolem2a  15066  summo  15068  zsum  15069  fsum  15071  sumsnf  15093  fsumcnv  15122  fsumcom2  15123  fsumshftm  15130  fsum0diag2  15132  prodeq2ii  15261  prodmolem3  15281  prodmolem2a  15282  prodmo  15284  zprod  15285  fprod  15289  prodsn  15310  prodsnf  15312  fprodcnv  15331  fprodcom2  15332  bpolylem  15396  bpolyval  15397  ruclem1  15578  pcmpt  16222  gsumvalx  17880  odfval  18654  odfvalALT  18655  odval  18656  telgsumfzslem  19102  telgsumfzs  19103  psrval  20136  psrass1lem  20151  mpfrcl  20292  evlsval  20293  evls1fval  20476  fsum2cn  23473  iunmbl2  24152  dvfsumlem1  24617  itgsubst  24640  q1pval  24741  r1pval  24744  rlimcnp2  25538  fsumdvdscom  25756  fsumdvdsmul  25766  ttgval  26655  fsumiunle  30540  msrfval  32779  poimirlem1  34887  poimirlem3  34889  poimirlem4  34890  poimirlem5  34891  poimirlem6  34892  poimirlem7  34893  poimirlem8  34894  poimirlem10  34896  poimirlem11  34897  poimirlem12  34898  poimirlem15  34901  poimirlem16  34902  poimirlem17  34903  poimirlem18  34904  poimirlem19  34905  poimirlem20  34906  poimirlem21  34907  poimirlem22  34908  poimirlem23  34909  poimirlem24  34910  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  poimirlem28  34914  cdleme31snd  37516  cdlemeg46c  37643  cdlemkid2  38054  cdlemk46  38078  cdlemk53b  38086  cdlemk53  38087  monotuz  39531  oddcomabszz  39534  fnwe2val  39642  fnwe2lem1  39643  fnwe2lem2  39644  mendval  39776  sumsnd  41276  climinf2mpt  41988  climinfmpt  41989  sge0f1o  42658  rnghmval  44156  dmmpossx2  44379