Theorem eceq1d 8537

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ec 8500

This theorem is referenced by:  brecop  8599  eroveu  8601  erov  8603  ecovcom  8612  ecovass  8613  ecovdi  8614  addsrmo  10829  mulsrmo  10830  addsrpr  10831  mulsrpr  10832  supsrlem  10867  supsr  10868  qus0  18814  qusinv  18815  qussub  18816  sylow2blem2  19226  frgpadd  19369  vrgpval  19373  vrgpinv  19375  frgpup3lem  19383  qusabl  19466  quscrng  20511  qustgplem  23272  pi1addval  24211  pi1xfrf  24216  pi1xfrval  24217  pi1xfrcnvlem  24219  pi1xfrcnv  24220  pi1cof  24222  pi1coval  24223  pi1coghm  24224  vitalilem3  24774  ismntoplly  31975  linedegen  34445  fvline  34446