Theorem eceq1d 8124

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

Syntax hints:   → wi 4   = wceq 1507  [cec 8083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-rab 3094  df-v 3414  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-br 4928  df-opab 4990  df-xp 5410  df-cnv 5412  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-ec 8087

This theorem is referenced by:  brecop  8186  eroveu  8188  erov  8190  ecovcom  8199  ecovass  8200  ecovdi  8201  addsrmo  10289  mulsrmo  10290  addsrpr  10291  mulsrpr  10292  supsrlem  10327  supsr  10328  qus0  18115  qusinv  18116  qussub  18117  sylow2blem2  18501  frgpadd  18643  vrgpval  18647  vrgpinv  18649  frgpup3lem  18657  qusabl  18735  quscrng  19728  qustgplem  22426  pi1addval  23349  pi1xfrf  23354  pi1xfrval  23355  pi1xfrcnvlem  23357  pi1xfrcnv  23358  pi1cof  23360  pi1coval  23361  pi1coghm  23362  vitalilem3  23908  ismntoplly  30901  linedegen  33095  fvline  33096