Theorem eceq1d 6528

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

Syntax hints:   -> wi 4   = wceq 1342   [cec 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115  df-in 3117  df-ss 3124  df-sn 3576  df-pr 3577  df-op 3579  df-br 3977  df-opab 4038  df-xp 4604  df-cnv 4606  df-dm 4608  df-rn 4609  df-res 4610  df-ima 4611  df-ec 6494

This theorem is referenced by:  brecop  6582  eroveu  6583  th3qlem1  6594  th3qlem2  6595  th3q  6597  oviec  6598  ecovcom  6599  ecovicom  6600  ecovass  6601  ecoviass  6602  ecovdi  6603  ecovidi  6604  mulidnq  7321  recexnq  7322  ltexnqq  7340  archnqq  7349  prarloclemarch2  7351  addnq0mo  7379  mulnq0mo  7380  addnnnq0  7381  mulnnnq0  7382  nqnq0a  7386  nqnq0m  7387  nq0a0  7389  nnanq0  7390  distrnq0  7391  mulcomnq0  7392  addassnq0  7394  addpinq1  7396  nq02m  7397  prarloclemlo  7426  prarloclem3  7429  prarloclem5  7432  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemm  7600  caucvgprlemdisj  7606  caucvgprlemloc  7607  caucvgprlemcl  7608  caucvgprlemladdfu  7609  caucvgprlemladdrl  7610  caucvgprlem1  7611  caucvgprlem2  7612  caucvgpr  7614  caucvgprprlemell  7617  caucvgprprlemelu  7618  caucvgprprlemcbv  7619  caucvgprprlemval  7620  caucvgprprlemnkeqj  7622  caucvgprprlemmu  7627  caucvgprprlemopl  7629  caucvgprprlemlol  7630  caucvgprprlemopu  7631  caucvgprprlemloc  7635  caucvgprprlemclphr  7637  caucvgprprlemexbt  7638  caucvgprprlem1  7641  caucvgprprlem2  7642  addsrmo  7675  mulsrmo  7676  addsrpr  7677  mulsrpr  7678  prsrriota  7720  caucvgsrlemfv  7723  caucvgsr  7734  suplocsrlemb  7738  suplocsrlempr  7739  suplocsrlem  7740  suplocsr  7741  pitonnlem2  7779  pitonn  7780  nntopi  7826  axcaucvglemval  7829