Theorem eceq1d 6417

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

Syntax hints:   -> wi 4   = wceq 1312   [cec 6379

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-sn 3497  df-pr 3498  df-op 3500  df-br 3894  df-opab 3948  df-xp 4503  df-cnv 4505  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-ec 6383

This theorem is referenced by:  brecop  6471  eroveu  6472  th3qlem1  6483  th3qlem2  6484  th3q  6486  oviec  6487  ecovcom  6488  ecovicom  6489  ecovass  6490  ecoviass  6491  ecovdi  6492  ecovidi  6493  mulidnq  7139  recexnq  7140  ltexnqq  7158  archnqq  7167  prarloclemarch2  7169  addnq0mo  7197  mulnq0mo  7198  addnnnq0  7199  mulnnnq0  7200  nqnq0a  7204  nqnq0m  7205  nq0a0  7207  nnanq0  7208  distrnq0  7209  mulcomnq0  7210  addassnq0  7212  addpinq1  7214  nq02m  7215  prarloclemlo  7244  prarloclem3  7247  prarloclem5  7250  caucvgprlemnkj  7416  caucvgprlemnbj  7417  caucvgprlemm  7418  caucvgprlemdisj  7424  caucvgprlemloc  7425  caucvgprlemcl  7426  caucvgprlemladdfu  7427  caucvgprlemladdrl  7428  caucvgprlem1  7429  caucvgprlem2  7430  caucvgpr  7432  caucvgprprlemell  7435  caucvgprprlemelu  7436  caucvgprprlemcbv  7437  caucvgprprlemval  7438  caucvgprprlemnkeqj  7440  caucvgprprlemmu  7445  caucvgprprlemopl  7447  caucvgprprlemlol  7448  caucvgprprlemopu  7449  caucvgprprlemloc  7453  caucvgprprlemclphr  7455  caucvgprprlemexbt  7456  caucvgprprlem1  7459  caucvgprprlem2  7460  addsrmo  7480  mulsrmo  7481  addsrpr  7482  mulsrpr  7483  prsrriota  7524  caucvgsrlemfv  7527  caucvgsr  7538  pitonnlem2  7576  pitonn  7577  nntopi  7623  axcaucvglemval  7626