Theorem eceq1d 6733

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

Syntax hints:   -> wi 4   = wceq 1395   [cec 6695

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-pr 3674  df-op 3676  df-br 4087  df-opab 4149  df-xp 4729  df-cnv 4731  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-ec 6699

This theorem is referenced by:  brecop  6789  eroveu  6790  th3qlem1  6801  th3qlem2  6802  th3q  6804  oviec  6805  ecovcom  6806  ecovicom  6807  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  mulidnq  7599  recexnq  7600  ltexnqq  7618  archnqq  7627  prarloclemarch2  7629  addnq0mo  7657  mulnq0mo  7658  addnnnq0  7659  mulnnnq0  7660  nqnq0a  7664  nqnq0m  7665  nq0a0  7667  nnanq0  7668  distrnq0  7669  mulcomnq0  7670  addassnq0  7672  addpinq1  7674  nq02m  7675  prarloclemlo  7704  prarloclem3  7707  prarloclem5  7710  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgprlem2  7890  caucvgpr  7892  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnkeqj  7900  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlemclphr  7915  caucvgprprlemexbt  7916  caucvgprprlem1  7919  caucvgprprlem2  7920  addsrmo  7953  mulsrmo  7954  addsrpr  7955  mulsrpr  7956  prsrriota  7998  caucvgsrlemfv  8001  caucvgsr  8012  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  suplocsr  8019  pitonnlem2  8057  pitonn  8058  nntopi  8104  axcaucvglemval  8107  qus0  13812  qusinv  13813  qussub  13814  quscrng  14537