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 1540  [cec 8672

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-ec 8676

This theorem is referenced by:  brecop  8786  eroveu  8788  erov  8790  ecovcom  8799  ecovass  8800  ecovdi  8801  addsrmo  11033  mulsrmo  11034  addsrpr  11035  mulsrpr  11036  supsrlem  11071  supsr  11072  qus0  19128  qusinv  19129  qussub  19130  sylow2blem2  19558  frgpadd  19700  vrgpval  19704  vrgpinv  19706  frgpup3lem  19714  qusabl  19802  quscrng  21200  pzriprnglem11  21408  pzriprnglem12  21409  qustgplem  24015  pi1addval  24955  pi1xfrf  24960  pi1xfrval  24961  pi1xfrcnvlem  24963  pi1xfrcnv  24964  pi1cof  24966  pi1coval  24967  pi1coghm  24968  vitalilem3  25518  elrlocbasi  33224  rlocaddval  33226  rlocmulval  33227  rloccring  33228  rloc0g  33229  rloc1r  33230  rlocf1  33231  idomsubr  33266  opprqusmulr  33469  zringfrac  33532  ismntoplly  34022  linedegen  36138  fvline  36139  aks5lem3a  42184  aks5lem5a  42186  aks5lem6  42187