Theorem eceq1d 8796

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  [cec 8753

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-cnv 5666  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-ec 8757

This theorem is used by:  brecop  8869  eroveu  8871  erov  8873  ecovcom  8882  ecovass  8883  ecovdi  8884  addsrmo  11197  mulsrmo  11198  addsrpr  11199  mulsrpr  11200  supsrlem  11235  supsr  11236  qus0  19454  qusinv  19455  qussub  19456  sylow2blem2  19886  frgpadd  20028  vrgpval  20032  vrgpinv  20034  frgpup3lem  20042  qusabl  20130  quscrng  21630  pzriprnglem11  21852  pzriprnglem12  21853  qustgplem  24495  pi1addval  25424  pi1xfrf  25429  pi1xfrval  25430  pi1xfrcnvlem  25432  pi1xfrcnv  25433  pi1cof  25435  pi1coval  25436  pi1coghm  25437  vitalilem3  25986  elrlocbasi  33927  rlocaddval  33929  rlocmulval  33930  rloccring  33931  rloc0g  33932  rloc1r  33933  rlocf1  33934  rlocisunit  33936  idomsubr  33975  opprqusmulr  34119  zringfrac  34189  ismntoplly  34768  linedegen  37123  fvline  37124  aks5lem3a  43505  aks5lem5a  43507  aks5lem6  43508