Theorem eceq1d 8785

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ec 8747

This theorem is referenced by:  brecop  8850  eroveu  8852  erov  8854  ecovcom  8863  ecovass  8864  ecovdi  8865  addsrmo  11113  mulsrmo  11114  addsrpr  11115  mulsrpr  11116  supsrlem  11151  supsr  11152  qus0  19207  qusinv  19208  qussub  19209  sylow2blem2  19639  frgpadd  19781  vrgpval  19785  vrgpinv  19787  frgpup3lem  19795  qusabl  19883  quscrng  21293  pzriprnglem11  21502  pzriprnglem12  21503  qustgplem  24129  pi1addval  25081  pi1xfrf  25086  pi1xfrval  25087  pi1xfrcnvlem  25089  pi1xfrcnv  25090  pi1cof  25092  pi1coval  25093  pi1coghm  25094  vitalilem3  25645  elrlocbasi  33270  rlocaddval  33272  rlocmulval  33273  rloccring  33274  rloc0g  33275  rloc1r  33276  rlocf1  33277  idomsubr  33311  opprqusmulr  33519  zringfrac  33582  ismntoplly  34026  linedegen  36144  fvline  36145  aks5lem3a  42190  aks5lem5a  42192  aks5lem6  42193