Theorem eceq1d 8520

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

Syntax hints:   → wi 4   = wceq 1542  [cec 8479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142  df-xp 5596  df-cnv 5598  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-ec 8483

This theorem is referenced by:  brecop  8582  eroveu  8584  erov  8586  ecovcom  8595  ecovass  8596  ecovdi  8597  addsrmo  10830  mulsrmo  10831  addsrpr  10832  mulsrpr  10833  supsrlem  10868  supsr  10869  qus0  18812  qusinv  18813  qussub  18814  sylow2blem2  19224  frgpadd  19367  vrgpval  19371  vrgpinv  19373  frgpup3lem  19381  qusabl  19464  quscrng  20509  qustgplem  23270  pi1addval  24209  pi1xfrf  24214  pi1xfrval  24215  pi1xfrcnvlem  24217  pi1xfrcnv  24218  pi1cof  24220  pi1coval  24221  pi1coghm  24222  vitalilem3  24772  ismntoplly  31971  linedegen  34441  fvline  34442