Theorem eceq1d 8770

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

Syntax hints:   → wi 4   = wceq 1533  [cec 8729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5688  df-cnv 5690  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ec 8733

This theorem is referenced by:  brecop  8835  eroveu  8837  erov  8839  ecovcom  8848  ecovass  8849  ecovdi  8850  addsrmo  11104  mulsrmo  11105  addsrpr  11106  mulsrpr  11107  supsrlem  11142  supsr  11143  qus0  19151  qusinv  19152  qussub  19153  sylow2blem2  19583  frgpadd  19725  vrgpval  19729  vrgpinv  19731  frgpup3lem  19739  qusabl  19827  quscrng  21182  pzriprnglem11  21424  pzriprnglem12  21425  qustgplem  24045  pi1addval  24995  pi1xfrf  25000  pi1xfrval  25001  pi1xfrcnvlem  25003  pi1xfrcnv  25004  pi1cof  25006  pi1coval  25007  pi1coghm  25008  vitalilem3  25559  elrlocbasi  33005  rlocaddval  33007  rlocmulval  33008  rloccring  33009  rloc0g  33010  rloc1r  33011  rlocf1  33012  idomsubr  33020  opprqusmulr  33227  zringfrac  33277  ismntoplly  33659  linedegen  35772  fvline  35773