Theorem eceq1d 6805

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

Syntax hints:   → wi 4   = wceq 1398  [cec 6767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112  df-opab 4174  df-xp 4757  df-cnv 4759  df-dm 4761  df-rn 4762  df-res 4763  df-ima 4764  df-ec 6771

This theorem is referenced by:  brecop  6861  eroveu  6862  th3qlem1  6873  th3qlem2  6874  th3q  6876  oviec  6877  ecovcom  6878  ecovicom  6879  ecovass  6880  ecoviass  6881  ecovdi  6882  ecovidi  6883  mulidnq  7709  recexnq  7710  ltexnqq  7728  archnqq  7737  prarloclemarch2  7739  addnq0mo  7767  mulnq0mo  7768  addnnnq0  7769  mulnnnq0  7770  nqnq0a  7774  nqnq0m  7775  nq0a0  7777  nnanq0  7778  distrnq0  7779  mulcomnq0  7780  addassnq0  7782  addpinq1  7784  nq02m  7785  prarloclemlo  7814  prarloclem3  7817  prarloclem5  7820  caucvgprlemnkj  7986  caucvgprlemnbj  7987  caucvgprlemm  7988  caucvgprlemdisj  7994  caucvgprlemloc  7995  caucvgprlemcl  7996  caucvgprlemladdfu  7997  caucvgprlemladdrl  7998  caucvgprlem1  7999  caucvgprlem2  8000  caucvgpr  8002  caucvgprprlemell  8005  caucvgprprlemelu  8006  caucvgprprlemcbv  8007  caucvgprprlemval  8008  caucvgprprlemnkeqj  8010  caucvgprprlemmu  8015  caucvgprprlemopl  8017  caucvgprprlemlol  8018  caucvgprprlemopu  8019  caucvgprprlemloc  8023  caucvgprprlemclphr  8025  caucvgprprlemexbt  8026  caucvgprprlem1  8029  caucvgprprlem2  8030  addsrmo  8063  mulsrmo  8064  addsrpr  8065  mulsrpr  8066  prsrriota  8108  caucvgsrlemfv  8111  caucvgsr  8122  suplocsrlemb  8126  suplocsrlempr  8127  suplocsrlem  8128  suplocsr  8129  pitonnlem2  8167  pitonn  8168  nntopi  8214  axcaucvglemval  8217  qus0  13973  qusinv  13974  qussub  13975  quscrng  14730