Theorem eceq1d 8408

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

Syntax hints:   → wi 4   = wceq 1543  [cec 8367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-xp 5542  df-cnv 5544  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-ec 8371

This theorem is referenced by:  brecop  8470  eroveu  8472  erov  8474  ecovcom  8483  ecovass  8484  ecovdi  8485  addsrmo  10652  mulsrmo  10653  addsrpr  10654  mulsrpr  10655  supsrlem  10690  supsr  10691  qus0  18556  qusinv  18557  qussub  18558  sylow2blem2  18964  frgpadd  19107  vrgpval  19111  vrgpinv  19113  frgpup3lem  19121  qusabl  19204  quscrng  20232  qustgplem  22972  pi1addval  23899  pi1xfrf  23904  pi1xfrval  23905  pi1xfrcnvlem  23907  pi1xfrcnv  23908  pi1cof  23910  pi1coval  23911  pi1coghm  23912  vitalilem3  24461  ismntoplly  31641  linedegen  34131  fvline  34132