Theorem eceq1d 6817

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

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

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 3218  df-in 3220  df-ss 3227  df-sn 3701  df-pr 3702  df-op 3704  df-br 4116  df-opab 4178  df-xp 4761  df-cnv 4763  df-dm 4765  df-rn 4766  df-res 4767  df-ima 4768  df-ec 6783

This theorem is referenced by:  brecop  6873  eroveu  6874  th3qlem1  6885  th3qlem2  6886  th3q  6888  oviec  6889  ecovcom  6890  ecovicom  6891  ecovass  6892  ecoviass  6893  ecovdi  6894  ecovidi  6895  mulidnq  7721  recexnq  7722  ltexnqq  7740  archnqq  7749  prarloclemarch2  7751  addnq0mo  7779  mulnq0mo  7780  addnnnq0  7781  mulnnnq0  7782  nqnq0a  7786  nqnq0m  7787  nq0a0  7789  nnanq0  7790  distrnq0  7791  mulcomnq0  7792  addassnq0  7794  addpinq1  7796  nq02m  7797  prarloclemlo  7826  prarloclem3  7829  prarloclem5  7832  caucvgprlemnkj  7998  caucvgprlemnbj  7999  caucvgprlemm  8000  caucvgprlemdisj  8006  caucvgprlemloc  8007  caucvgprlemcl  8008  caucvgprlemladdfu  8009  caucvgprlemladdrl  8010  caucvgprlem1  8011  caucvgprlem2  8012  caucvgpr  8014  caucvgprprlemell  8017  caucvgprprlemelu  8018  caucvgprprlemcbv  8019  caucvgprprlemval  8020  caucvgprprlemnkeqj  8022  caucvgprprlemmu  8027  caucvgprprlemopl  8029  caucvgprprlemlol  8030  caucvgprprlemopu  8031  caucvgprprlemloc  8035  caucvgprprlemclphr  8037  caucvgprprlemexbt  8038  caucvgprprlem1  8041  caucvgprprlem2  8042  addsrmo  8075  mulsrmo  8076  addsrpr  8077  mulsrpr  8078  prsrriota  8120  caucvgsrlemfv  8123  caucvgsr  8134  suplocsrlemb  8138  suplocsrlempr  8139  suplocsrlem  8140  suplocsr  8141  pitonnlem2  8179  pitonn  8180  nntopi  8226  axcaucvglemval  8229  qus0  13993  qusinv  13994  qussub  13995  quscrng  14812