Theorem eceq1d 8737

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ec 8698

This theorem is used by:  brecop  8810  eroveu  8812  erov  8814  ecovcom  8823  ecovass  8824  ecovdi  8825  addsrmo  11082  mulsrmo  11083  addsrpr  11084  mulsrpr  11085  supsrlem  11120  supsr  11121  qus0  19317  qusinv  19318  qussub  19319  sylow2blem2  19748  frgpadd  19890  vrgpval  19894  vrgpinv  19896  frgpup3lem  19904  qusabl  19992  quscrng  21486  pzriprnglem11  21704  pzriprnglem12  21705  qustgplem  24347  pi1addval  25276  pi1xfrf  25281  pi1xfrval  25282  pi1xfrcnvlem  25284  pi1xfrcnv  25285  pi1cof  25287  pi1coval  25288  pi1coghm  25289  vitalilem3  25838  elrlocbasi  33707  rlocaddval  33709  rlocmulval  33710  rloccring  33711  rloc0g  33712  rloc1r  33713  rlocf1  33714  rlocisunit  33716  idomsubr  33750  opprqusmulr  33893  zringfrac  33964  ismntoplly  34535  linedegen  36723  fvline  36724  aks5lem3a  43055  aks5lem5a  43057  aks5lem6  43058