Theorem eceq1d 8738

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

Syntax hints:   → wi 4   = wceq 1541  [cec 8697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  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 8701

This theorem is referenced by:  brecop  8800  eroveu  8802  erov  8804  ecovcom  8813  ecovass  8814  ecovdi  8815  addsrmo  11064  mulsrmo  11065  addsrpr  11066  mulsrpr  11067  supsrlem  11102  supsr  11103  qus0  19062  qusinv  19063  qussub  19064  sylow2blem2  19483  frgpadd  19625  vrgpval  19629  vrgpinv  19631  frgpup3lem  19639  qusabl  19727  quscrng  20870  qustgplem  23616  pi1addval  24555  pi1xfrf  24560  pi1xfrval  24561  pi1xfrcnvlem  24563  pi1xfrcnv  24564  pi1cof  24566  pi1coval  24567  pi1coghm  24568  vitalilem3  25118  opprqusmulr  32593  ismntoplly  32993  linedegen  35103  fvline  35104