Theorem eceq1d 6781

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 6780	. 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 6743

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-opab 4156  df-xp 4737  df-cnv 4739  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-ec 6747

This theorem is referenced by:  brecop  6837  eroveu  6838  th3qlem1  6849  th3qlem2  6850  th3q  6852  oviec  6853  ecovcom  6854  ecovicom  6855  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  mulidnq  7652  recexnq  7653  ltexnqq  7671  archnqq  7680  prarloclemarch2  7682  addnq0mo  7710  mulnq0mo  7711  addnnnq0  7712  mulnnnq0  7713  nqnq0a  7717  nqnq0m  7718  nq0a0  7720  nnanq0  7721  distrnq0  7722  mulcomnq0  7723  addassnq0  7725  addpinq1  7727  nq02m  7728  prarloclemlo  7757  prarloclem3  7760  prarloclem5  7763  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem1  7942  caucvgprlem2  7943  caucvgpr  7945  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemnkeqj  7953  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  caucvgprprlem1  7972  caucvgprprlem2  7973  addsrmo  8006  mulsrmo  8007  addsrpr  8008  mulsrpr  8009  prsrriota  8051  caucvgsrlemfv  8054  caucvgsr  8065  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  suplocsr  8072  pitonnlem2  8110  pitonn  8111  nntopi  8157  axcaucvglemval  8160  qus0  13885  qusinv  13886  qussub  13887  quscrng  14612