Theorem eceq1d 6368

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

Syntax hints:   → wi 4   = wceq 1296  [cec 6330

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 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-in 3019  df-ss 3026  df-sn 3472  df-pr 3473  df-op 3475  df-br 3868  df-opab 3922  df-xp 4473  df-cnv 4475  df-dm 4477  df-rn 4478  df-res 4479  df-ima 4480  df-ec 6334

This theorem is referenced by:  brecop  6422  eroveu  6423  th3qlem1  6434  th3qlem2  6435  th3q  6437  oviec  6438  ecovcom  6439  ecovicom  6440  ecovass  6441  ecoviass  6442  ecovdi  6443  ecovidi  6444  mulidnq  7045  recexnq  7046  ltexnqq  7064  archnqq  7073  prarloclemarch2  7075  addnq0mo  7103  mulnq0mo  7104  addnnnq0  7105  mulnnnq0  7106  nqnq0a  7110  nqnq0m  7111  nq0a0  7113  nnanq0  7114  distrnq0  7115  mulcomnq0  7116  addassnq0  7118  addpinq1  7120  nq02m  7121  prarloclemlo  7150  prarloclem3  7153  prarloclem5  7156  caucvgprlemnkj  7322  caucvgprlemnbj  7323  caucvgprlemm  7324  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlemcl  7332  caucvgprlemladdfu  7333  caucvgprlemladdrl  7334  caucvgprlem1  7335  caucvgprlem2  7336  caucvgpr  7338  caucvgprprlemell  7341  caucvgprprlemelu  7342  caucvgprprlemcbv  7343  caucvgprprlemval  7344  caucvgprprlemnkeqj  7346  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemlol  7354  caucvgprprlemopu  7355  caucvgprprlemloc  7359  caucvgprprlemclphr  7361  caucvgprprlemexbt  7362  caucvgprprlem1  7365  caucvgprprlem2  7366  addsrmo  7386  mulsrmo  7387  addsrpr  7388  mulsrpr  7389  prsrriota  7430  caucvgsrlemfv  7433  caucvgsr  7444  pitonnlem2  7481  pitonn  7482  nntopi  7526  axcaucvglemval  7529