Theorem eceq1d 8665

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 8664	. 2 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
3	1, 2	syl 17	1 ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1540  [cec 8623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ec 8627

This theorem is referenced by:  brecop  8737  eroveu  8739  erov  8741  ecovcom  8750  ecovass  8751  ecovdi  8752  addsrmo  10967  mulsrmo  10968  addsrpr  10969  mulsrpr  10970  supsrlem  11005  supsr  11006  qus0  19068  qusinv  19069  qussub  19070  sylow2blem2  19500  frgpadd  19642  vrgpval  19646  vrgpinv  19648  frgpup3lem  19656  qusabl  19744  quscrng  21190  pzriprnglem11  21398  pzriprnglem12  21399  qustgplem  24006  pi1addval  24946  pi1xfrf  24951  pi1xfrval  24952  pi1xfrcnvlem  24954  pi1xfrcnv  24955  pi1cof  24957  pi1coval  24958  pi1coghm  24959  vitalilem3  25509  elrlocbasi  33215  rlocaddval  33217  rlocmulval  33218  rloccring  33219  rloc0g  33220  rloc1r  33221  rlocf1  33222  idomsubr  33257  opprqusmulr  33437  zringfrac  33500  ismntoplly  34008  linedegen  36137  fvline  36138  aks5lem3a  42182  aks5lem5a  42184  aks5lem6  42185