Theorem eceq1d 6737

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 6736	. 2 |- ( A = B -> [ A ] C = [ B ] C )
3	1, 2	syl 14	1 |- ( ph -> [ A ] C = [ B ] C )

Syntax hints:   -> wi 4   = wceq 1397   [cec 6699

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-opab 4151  df-xp 4731  df-cnv 4733  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-ec 6703

This theorem is referenced by:  brecop  6793  eroveu  6794  th3qlem1  6805  th3qlem2  6806  th3q  6808  oviec  6809  ecovcom  6810  ecovicom  6811  ecovass  6812  ecoviass  6813  ecovdi  6814  ecovidi  6815  mulidnq  7608  recexnq  7609  ltexnqq  7627  archnqq  7636  prarloclemarch2  7638  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  mulnnnq0  7669  nqnq0a  7673  nqnq0m  7674  nq0a0  7676  nnanq0  7677  distrnq0  7678  mulcomnq0  7679  addassnq0  7681  addpinq1  7683  nq02m  7684  prarloclemlo  7713  prarloclem3  7716  prarloclem5  7719  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgprlem2  7899  caucvgpr  7901  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnkeqj  7909  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  caucvgprprlem1  7928  caucvgprprlem2  7929  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  prsrriota  8007  caucvgsrlemfv  8010  caucvgsr  8021  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  suplocsr  8028  pitonnlem2  8066  pitonn  8067  nntopi  8113  axcaucvglemval  8116  qus0  13821  qusinv  13822  qussub  13823  quscrng  14546