Theorem eceq1d 6686

Description: Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)

Hypothesis

Ref	Expression
eceq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eceq1d	⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)

Proof of Theorem eceq1d

Step	Hyp	Ref	Expression
1		eceq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eceq1 6685	. 2 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
3	1, 2	syl 14	1 ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1375  [cec 6648

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-v 2781  df-un 3181  df-in 3183  df-ss 3190  df-sn 3652  df-pr 3653  df-op 3655  df-br 4063  df-opab 4125  df-xp 4702  df-cnv 4704  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-ec 6652

This theorem is referenced by:  brecop  6742  eroveu  6743  th3qlem1  6754  th3qlem2  6755  th3q  6757  oviec  6758  ecovcom  6759  ecovicom  6760  ecovass  6761  ecoviass  6762  ecovdi  6763  ecovidi  6764  mulidnq  7544  recexnq  7545  ltexnqq  7563  archnqq  7572  prarloclemarch2  7574  addnq0mo  7602  mulnq0mo  7603  addnnnq0  7604  mulnnnq0  7605  nqnq0a  7609  nqnq0m  7610  nq0a0  7612  nnanq0  7613  distrnq0  7614  mulcomnq0  7615  addassnq0  7617  addpinq1  7619  nq02m  7620  prarloclemlo  7649  prarloclem3  7652  prarloclem5  7655  caucvgprlemnkj  7821  caucvgprlemnbj  7822  caucvgprlemm  7823  caucvgprlemdisj  7829  caucvgprlemloc  7830  caucvgprlemcl  7831  caucvgprlemladdfu  7832  caucvgprlemladdrl  7833  caucvgprlem1  7834  caucvgprlem2  7835  caucvgpr  7837  caucvgprprlemell  7840  caucvgprprlemelu  7841  caucvgprprlemcbv  7842  caucvgprprlemval  7843  caucvgprprlemnkeqj  7845  caucvgprprlemmu  7850  caucvgprprlemopl  7852  caucvgprprlemlol  7853  caucvgprprlemopu  7854  caucvgprprlemloc  7858  caucvgprprlemclphr  7860  caucvgprprlemexbt  7861  caucvgprprlem1  7864  caucvgprprlem2  7865  addsrmo  7898  mulsrmo  7899  addsrpr  7900  mulsrpr  7901  prsrriota  7943  caucvgsrlemfv  7946  caucvgsr  7957  suplocsrlemb  7961  suplocsrlempr  7962  suplocsrlem  7963  suplocsr  7964  pitonnlem2  8002  pitonn  8003  nntopi  8049  axcaucvglemval  8052  qus0  13738  qusinv  13739  qussub  13740  quscrng  14462