Theorem eceq1d 7670

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

Syntax hints:   → wi 4   = wceq 1475  [cec 7627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ec 7631

This theorem is referenced by:  brecop  7727  eroveu  7729  erov  7731  ecovcom  7741  ecovass  7742  ecovdi  7743  addsrmo  9773  mulsrmo  9774  addsrpr  9775  mulsrpr  9776  supsrlem  9811  supsr  9812  qus0  17475  qusinv  17476  qussub  17477  sylow2blem2  17859  frgpadd  17999  vrgpval  18003  vrgpinv  18005  frgpup3lem  18013  qusabl  18091  quscrng  19061  qustgplem  21734  pi1addval  22656  pi1xfrf  22661  pi1xfrval  22662  pi1xfrcnvlem  22664  pi1xfrcnv  22665  pi1cof  22667  pi1coval  22668  pi1coghm  22669  vitalilem3  23185  ismntoplly  29397  linedegen  31420  fvline  31421