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  7084  mpomptsx  8017  dmmpossx  8019  fmpox  8020  ovmptss  8043  fmpoco  8045  xpf1o  9077  hsmexlem2  10349  iundom2g  10462  sumeq2ii  15655  summolem3  15676  summolem2a  15677  summo  15679  zsum  15680  fsum  15682  sumsnf  15705  fsumcnv  15735  fsumcom2  15736  fsumshftm  15743  fsum0diag2  15745  prodeq2ii  15876  prodmolem3  15898  prodmolem2a  15899  prodmo  15901  zprod  15902  fprod  15906  prodsn  15927  prodsnf  15929  fprodcnv  15948  fprodcom2  15949  bpolylem  16013  bpolyval  16014  ruclem1  16198  pcmpt  16863  gsumvalx  18644  odfval  19507  odfvalALT  19508  odval  19509  telgsumfzslem  19963  telgsumfzs  19964  rnghmval  20420  psrval  21895  psrass1lem  21912  mpfrcl  22063  evlsval  22064  evls1fval  22284  fsum2cn  24838  iunmbl2  25524  dvfsumlem1  25993  itgsubst  26016  q1pval  26120  r1pval  26123  rlimcnp2  26930  fsumdvdscom  27148  fsumdvdsmul  27158  mulsval  28101  precsexlemcbv  28198  precsexlem3  28201  fsumiunle  32902  msrfval  35719  weiunval  36644  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  poimirlem1  37942  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  cdleme31snd  40832  cdlemeg46c  40959  cdlemkid2  41370  cdlemk46  41394  cdlemk53b  41402  cdlemk53  41403  deg1gprod  42579  fmpocos  42675  monotuz  43369  oddcomabszz  43372  fnwe2val  43477  fnwe2lem1  43478  fnwe2lem2  43479  mendval  43607  sumsnd  45457  climinf2mpt  46142  climinfmpt  46143  sge0f1o  46810  grtri  48410  dmmpossx2  48807  dfswapf2  49730