Theorem eceq1d 6596

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

Syntax hints:   -> wi 4   = wceq 1364   [cec 6558

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-pr 3614  df-op 3616  df-br 4019  df-opab 4080  df-xp 4650  df-cnv 4652  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-ec 6562

This theorem is referenced by:  brecop  6652  eroveu  6653  th3qlem1  6664  th3qlem2  6665  th3q  6667  oviec  6668  ecovcom  6669  ecovicom  6670  ecovass  6671  ecoviass  6672  ecovdi  6673  ecovidi  6674  mulidnq  7419  recexnq  7420  ltexnqq  7438  archnqq  7447  prarloclemarch2  7449  addnq0mo  7477  mulnq0mo  7478  addnnnq0  7479  mulnnnq0  7480  nqnq0a  7484  nqnq0m  7485  nq0a0  7487  nnanq0  7488  distrnq0  7489  mulcomnq0  7490  addassnq0  7492  addpinq1  7494  nq02m  7495  prarloclemlo  7524  prarloclem3  7527  prarloclem5  7530  caucvgprlemnkj  7696  caucvgprlemnbj  7697  caucvgprlemm  7698  caucvgprlemdisj  7704  caucvgprlemloc  7705  caucvgprlemcl  7706  caucvgprlemladdfu  7707  caucvgprlemladdrl  7708  caucvgprlem1  7709  caucvgprlem2  7710  caucvgpr  7712  caucvgprprlemell  7715  caucvgprprlemelu  7716  caucvgprprlemcbv  7717  caucvgprprlemval  7718  caucvgprprlemnkeqj  7720  caucvgprprlemmu  7725  caucvgprprlemopl  7727  caucvgprprlemlol  7728  caucvgprprlemopu  7729  caucvgprprlemloc  7733  caucvgprprlemclphr  7735  caucvgprprlemexbt  7736  caucvgprprlem1  7739  caucvgprprlem2  7740  addsrmo  7773  mulsrmo  7774  addsrpr  7775  mulsrpr  7776  prsrriota  7818  caucvgsrlemfv  7821  caucvgsr  7832  suplocsrlemb  7836  suplocsrlempr  7837  suplocsrlem  7838  suplocsr  7839  pitonnlem2  7877  pitonn  7878  nntopi  7924  axcaucvglemval  7927  qus0  13191  qusinv  13192  qussub  13193  quscrng  13864