Theorem eceq1d 6585

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

Syntax hints:   → wi 4   = wceq 1363  [cec 6547

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145  df-in 3147  df-ss 3154  df-sn 3610  df-pr 3611  df-op 3613  df-br 4016  df-opab 4077  df-xp 4644  df-cnv 4646  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-ec 6551

This theorem is referenced by:  brecop  6639  eroveu  6640  th3qlem1  6651  th3qlem2  6652  th3q  6654  oviec  6655  ecovcom  6656  ecovicom  6657  ecovass  6658  ecoviass  6659  ecovdi  6660  ecovidi  6661  mulidnq  7402  recexnq  7403  ltexnqq  7421  archnqq  7430  prarloclemarch2  7432  addnq0mo  7460  mulnq0mo  7461  addnnnq0  7462  mulnnnq0  7463  nqnq0a  7467  nqnq0m  7468  nq0a0  7470  nnanq0  7471  distrnq0  7472  mulcomnq0  7473  addassnq0  7475  addpinq1  7477  nq02m  7478  prarloclemlo  7507  prarloclem3  7510  prarloclem5  7513  caucvgprlemnkj  7679  caucvgprlemnbj  7680  caucvgprlemm  7681  caucvgprlemdisj  7687  caucvgprlemloc  7688  caucvgprlemcl  7689  caucvgprlemladdfu  7690  caucvgprlemladdrl  7691  caucvgprlem1  7692  caucvgprlem2  7693  caucvgpr  7695  caucvgprprlemell  7698  caucvgprprlemelu  7699  caucvgprprlemcbv  7700  caucvgprprlemval  7701  caucvgprprlemnkeqj  7703  caucvgprprlemmu  7708  caucvgprprlemopl  7710  caucvgprprlemlol  7711  caucvgprprlemopu  7712  caucvgprprlemloc  7716  caucvgprprlemclphr  7718  caucvgprprlemexbt  7719  caucvgprprlem1  7722  caucvgprprlem2  7723  addsrmo  7756  mulsrmo  7757  addsrpr  7758  mulsrpr  7759  prsrriota  7801  caucvgsrlemfv  7804  caucvgsr  7815  suplocsrlemb  7819  suplocsrlempr  7820  suplocsrlem  7821  suplocsr  7822  pitonnlem2  7860  pitonn  7861  nntopi  7907  axcaucvglemval  7910  quscrng  13720