Theorem eceq1d 6816

Description: Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)

Hypothesis

Ref	Expression
eceq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
eceq1d	|- ( ph -> [ A ] C = [ B ] C )

Proof of Theorem eceq1d

Step	Hyp	Ref	Expression
1		eceq1d.1	. 2 |- ( ph -> A = B )
2		eceq1 6815	. 2 |- ( A = B -> [ A ] C = [ B ] C )
3	1, 2	syl 14	1 |- ( ph -> [ A ] C = [ B ] C )

Syntax hints:   -> wi 4   = wceq 1398   [cec 6778

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 3700  df-pr 3701  df-op 3703  df-br 4115  df-opab 4177  df-xp 4760  df-cnv 4762  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-ec 6782

This theorem is referenced by:  brecop  6872  eroveu  6873  th3qlem1  6884  th3qlem2  6885  th3q  6887  oviec  6888  ecovcom  6889  ecovicom  6890  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  mulidnq  7720  recexnq  7721  ltexnqq  7739  archnqq  7748  prarloclemarch2  7750  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  mulnnnq0  7781  nqnq0a  7785  nqnq0m  7786  nq0a0  7788  nnanq0  7789  distrnq0  7790  mulcomnq0  7791  addassnq0  7793  addpinq1  7795  nq02m  7796  prarloclemlo  7825  prarloclem3  7828  prarloclem5  7831  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgprlem2  8011  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemelu  8017  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexbt  8037  caucvgprprlem1  8040  caucvgprprlem2  8041  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  prsrriota  8119  caucvgsrlemfv  8122  caucvgsr  8133  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  suplocsr  8140  pitonnlem2  8178  pitonn  8179  nntopi  8225  axcaucvglemval  8228  qus0  13988  qusinv  13989  qussub  13990  quscrng  14807