Theorem eceq1d 6843

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   [cec 6805

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131  df-opab 4193  df-xp 4780  df-cnv 4782  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-ec 6809

This theorem is used by:  brecop  6899  eroveu  6900  th3qlem1  6911  th3qlem2  6912  th3q  6914  oviec  6915  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  mulidnq  7757  recexnq  7758  ltexnqq  7776  archnqq  7785  prarloclemarch2  7787  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  mulnnnq0  7818  nqnq0a  7822  nqnq0m  7823  nq0a0  7825  nnanq0  7826  distrnq0  7827  mulcomnq0  7828  addassnq0  7830  addpinq1  7832  nq02m  7833  prarloclemlo  7862  prarloclem3  7865  prarloclem5  7868  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgprlem2  8048  caucvgpr  8050  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkeqj  8058  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexbt  8074  caucvgprprlem1  8077  caucvgprprlem2  8078  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  prsrriota  8156  caucvgsrlemfv  8159  caucvgsr  8170  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  suplocsr  8177  pitonnlem2  8215  pitonn  8216  nntopi  8262  axcaucvglemval  8265  qus0  14091  qusinv  14092  qussub  14093  quscrng  14954