Theorem eceq1d 8723

Description: Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)

Hypothesis

Ref	Expression
eceq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eceq1d	⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)

Proof of Theorem eceq1d

Step	Hyp	Ref	Expression
1		eceq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eceq1 8722	. 2 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
3	1, 2	syl 18	1 ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1563  [cec 8680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-xp 5658  df-cnv 5660  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-ec 8684

This theorem is referenced by:  brecop  8796  eroveu  8798  erov  8800  ecovcom  8809  ecovass  8810  ecovdi  8811  addsrmo  11046  mulsrmo  11047  addsrpr  11048  mulsrpr  11049  supsrlem  11084  supsr  11085  qus0  19251  qusinv  19252  qussub  19253  sylow2blem2  19682  frgpadd  19824  vrgpval  19828  vrgpinv  19830  frgpup3lem  19838  qusabl  19926  quscrng  21385  pzriprnglem11  21601  pzriprnglem12  21602  qustgplem  24239  pi1addval  25168  pi1xfrf  25173  pi1xfrval  25174  pi1xfrcnvlem  25176  pi1xfrcnv  25177  pi1cof  25179  pi1coval  25180  pi1coghm  25181  vitalilem3  25730  elrlocbasi  33500  rlocaddval  33502  rlocmulval  33503  rloccring  33504  rloc0g  33505  rloc1r  33506  rlocf1  33507  rlocisunit  33509  idomsubr  33545  opprqusmulr  33690  zringfrac  33761  ismntoplly  34332  linedegen  36506  fvline  36507  aks5lem3a  42818  aks5lem5a  42820  aks5lem6  42821