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 5105  df-opab 5167  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  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  19248  qusinv  19249  qussub  19250  sylow2blem2  19679  frgpadd  19821  vrgpval  19825  vrgpinv  19827  frgpup3lem  19835  qusabl  19923  quscrng  21382  pzriprnglem11  21598  pzriprnglem12  21599  qustgplem  24235  pi1addval  25164  pi1xfrf  25169  pi1xfrval  25170  pi1xfrcnvlem  25172  pi1xfrcnv  25173  pi1cof  25175  pi1coval  25176  pi1coghm  25177  vitalilem3  25726  elrlocbasi  33495  rlocaddval  33497  rlocmulval  33498  rloccring  33499  rloc0g  33500  rloc1r  33501  rlocf1  33502  rlocisunit  33504  idomsubr  33540  opprqusmulr  33685  zringfrac  33756  ismntoplly  34327  linedegen  36501  fvline  36502  aks5lem3a  42813  aks5lem5a  42815  aks5lem6  42816