Theorem eceq1d 8744

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

Syntax hints:   → wi 4   = wceq 1539  [cec 8703

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ec 8707

This theorem is referenced by:  brecop  8806  eroveu  8808  erov  8810  ecovcom  8819  ecovass  8820  ecovdi  8821  addsrmo  11070  mulsrmo  11071  addsrpr  11072  mulsrpr  11073  supsrlem  11108  supsr  11109  qus0  19104  qusinv  19105  qussub  19106  sylow2blem2  19530  frgpadd  19672  vrgpval  19676  vrgpinv  19678  frgpup3lem  19686  qusabl  19774  quscrng  21029  pzriprnglem11  21260  pzriprnglem12  21261  qustgplem  23845  pi1addval  24795  pi1xfrf  24800  pi1xfrval  24801  pi1xfrcnvlem  24803  pi1xfrcnv  24804  pi1cof  24806  pi1coval  24807  pi1coghm  24808  vitalilem3  25359  opprqusmulr  32879  ismntoplly  33303  linedegen  35419  fvline  35420