Theorem eceq1d 6570

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

Syntax hints:   → wi 4   = wceq 1353  [cec 6532

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004  df-opab 4065  df-xp 4632  df-cnv 4634  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-ec 6536

This theorem is referenced by:  brecop  6624  eroveu  6625  th3qlem1  6636  th3qlem2  6637  th3q  6639  oviec  6640  ecovcom  6641  ecovicom  6642  ecovass  6643  ecoviass  6644  ecovdi  6645  ecovidi  6646  mulidnq  7387  recexnq  7388  ltexnqq  7406  archnqq  7415  prarloclemarch2  7417  addnq0mo  7445  mulnq0mo  7446  addnnnq0  7447  mulnnnq0  7448  nqnq0a  7452  nqnq0m  7453  nq0a0  7455  nnanq0  7456  distrnq0  7457  mulcomnq0  7458  addassnq0  7460  addpinq1  7462  nq02m  7463  prarloclemlo  7492  prarloclem3  7495  prarloclem5  7498  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgprlem2  7678  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  addsrmo  7741  mulsrmo  7742  addsrpr  7743  mulsrpr  7744  prsrriota  7786  caucvgsrlemfv  7789  caucvgsr  7800  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  suplocsr  7807  pitonnlem2  7845  pitonn  7846  nntopi  7892  axcaucvglemval  7895