Theorem eceq1d 6473

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

Syntax hints:   → wi 4   = wceq 1332  [cec 6435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-sn 3538  df-pr 3539  df-op 3541  df-br 3938  df-opab 3998  df-xp 4553  df-cnv 4555  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-ec 6439

This theorem is referenced by:  brecop  6527  eroveu  6528  th3qlem1  6539  th3qlem2  6540  th3q  6542  oviec  6543  ecovcom  6544  ecovicom  6545  ecovass  6546  ecoviass  6547  ecovdi  6548  ecovidi  6549  mulidnq  7221  recexnq  7222  ltexnqq  7240  archnqq  7249  prarloclemarch2  7251  addnq0mo  7279  mulnq0mo  7280  addnnnq0  7281  mulnnnq0  7282  nqnq0a  7286  nqnq0m  7287  nq0a0  7289  nnanq0  7290  distrnq0  7291  mulcomnq0  7292  addassnq0  7294  addpinq1  7296  nq02m  7297  prarloclemlo  7326  prarloclem3  7329  prarloclem5  7332  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemdisj  7506  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem1  7511  caucvgprlem2  7512  caucvgpr  7514  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemnkeqj  7522  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemloc  7535  caucvgprprlemclphr  7537  caucvgprprlemexbt  7538  caucvgprprlem1  7541  caucvgprprlem2  7542  addsrmo  7575  mulsrmo  7576  addsrpr  7577  mulsrpr  7578  prsrriota  7620  caucvgsrlemfv  7623  caucvgsr  7634  suplocsrlemb  7638  suplocsrlempr  7639  suplocsrlem  7640  suplocsr  7641  pitonnlem2  7679  pitonn  7680  nntopi  7726  axcaucvglemval  7729