Theorem eceq1d 8668

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

Syntax hints:   → wi 4   = wceq 1541  [cec 8626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ec 8630

This theorem is referenced by:  brecop  8740  eroveu  8742  erov  8744  ecovcom  8753  ecovass  8754  ecovdi  8755  addsrmo  10971  mulsrmo  10972  addsrpr  10973  mulsrpr  10974  supsrlem  11009  supsr  11010  qus0  19103  qusinv  19104  qussub  19105  sylow2blem2  19535  frgpadd  19677  vrgpval  19681  vrgpinv  19683  frgpup3lem  19691  qusabl  19779  quscrng  21222  pzriprnglem11  21430  pzriprnglem12  21431  qustgplem  24037  pi1addval  24976  pi1xfrf  24981  pi1xfrval  24982  pi1xfrcnvlem  24984  pi1xfrcnv  24985  pi1cof  24987  pi1coval  24988  pi1coghm  24989  vitalilem3  25539  elrlocbasi  33240  rlocaddval  33242  rlocmulval  33243  rloccring  33244  rloc0g  33245  rloc1r  33246  rlocf1  33247  idomsubr  33282  opprqusmulr  33463  zringfrac  33526  ismntoplly  34059  linedegen  36208  fvline  36209  aks5lem3a  42302  aks5lem5a  42304  aks5lem6  42305