Theorem eceq1d 8711

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ec 8673

This theorem is referenced by:  brecop  8783  eroveu  8785  erov  8787  ecovcom  8796  ecovass  8797  ecovdi  8798  addsrmo  11026  mulsrmo  11027  addsrpr  11028  mulsrpr  11029  supsrlem  11064  supsr  11065  qus0  19121  qusinv  19122  qussub  19123  sylow2blem2  19551  frgpadd  19693  vrgpval  19697  vrgpinv  19699  frgpup3lem  19707  qusabl  19795  quscrng  21193  pzriprnglem11  21401  pzriprnglem12  21402  qustgplem  24008  pi1addval  24948  pi1xfrf  24953  pi1xfrval  24954  pi1xfrcnvlem  24956  pi1xfrcnv  24957  pi1cof  24959  pi1coval  24960  pi1coghm  24961  vitalilem3  25511  elrlocbasi  33217  rlocaddval  33219  rlocmulval  33220  rloccring  33221  rloc0g  33222  rloc1r  33223  rlocf1  33224  idomsubr  33259  opprqusmulr  33462  zringfrac  33525  ismntoplly  34015  linedegen  36131  fvline  36132  aks5lem3a  42177  aks5lem5a  42179  aks5lem6  42180