Theorem eceq1d 6625

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 6624	. 2 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
3	1, 2	syl 14	1 ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1364  [cec 6587

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031  df-opab 4092  df-xp 4666  df-cnv 4668  df-dm 4670  df-rn 4671  df-res 4672  df-ima 4673  df-ec 6591

This theorem is referenced by:  brecop  6681  eroveu  6682  th3qlem1  6693  th3qlem2  6694  th3q  6696  oviec  6697  ecovcom  6698  ecovicom  6699  ecovass  6700  ecoviass  6701  ecovdi  6702  ecovidi  6703  mulidnq  7451  recexnq  7452  ltexnqq  7470  archnqq  7479  prarloclemarch2  7481  addnq0mo  7509  mulnq0mo  7510  addnnnq0  7511  mulnnnq0  7512  nqnq0a  7516  nqnq0m  7517  nq0a0  7519  nnanq0  7520  distrnq0  7521  mulcomnq0  7522  addassnq0  7524  addpinq1  7526  nq02m  7527  prarloclemlo  7556  prarloclem3  7559  prarloclem5  7562  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgprlem2  7742  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnkeqj  7752  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  caucvgprprlem1  7771  caucvgprprlem2  7772  addsrmo  7805  mulsrmo  7806  addsrpr  7807  mulsrpr  7808  prsrriota  7850  caucvgsrlemfv  7853  caucvgsr  7864  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  suplocsr  7871  pitonnlem2  7909  pitonn  7910  nntopi  7956  axcaucvglemval  7959  qus0  13308  qusinv  13309  qussub  13310  quscrng  14032