Theorem eceq1d 8714

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

Syntax hints:   → wi 4   = wceq 1559  [cec 8671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5651  df-cnv 5653  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-ec 8675

This theorem is referenced by:  brecop  8787  eroveu  8789  erov  8791  ecovcom  8800  ecovass  8801  ecovdi  8802  addsrmo  11028  mulsrmo  11029  addsrpr  11030  mulsrpr  11031  supsrlem  11066  supsr  11067  qus0  19213  qusinv  19214  qussub  19215  sylow2blem2  19644  frgpadd  19786  vrgpval  19790  vrgpinv  19792  frgpup3lem  19800  qusabl  19888  quscrng  21333  pzriprnglem11  21523  pzriprnglem12  21524  qustgplem  24161  pi1addval  25090  pi1xfrf  25095  pi1xfrval  25096  pi1xfrcnvlem  25098  pi1xfrcnv  25099  pi1cof  25101  pi1coval  25102  pi1coghm  25103  vitalilem3  25652  elrlocbasi  33409  rlocaddval  33411  rlocmulval  33412  rloccring  33413  rloc0g  33414  rloc1r  33415  rlocf1  33416  rlocisunit  33418  idomsubr  33457  opprqusmulr  33640  zringfrac  33711  ismntoplly  34283  linedegen  36457  fvline  36458  aks5lem3a  42770  aks5lem5a  42772  aks5lem6  42773