Theorem eceq1d 6629

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-pr 3630  df-op 3632  df-br 4035  df-opab 4096  df-xp 4670  df-cnv 4672  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-ec 6595

This theorem is referenced by:  brecop  6685  eroveu  6686  th3qlem1  6697  th3qlem2  6698  th3q  6700  oviec  6701  ecovcom  6702  ecovicom  6703  ecovass  6704  ecoviass  6705  ecovdi  6706  ecovidi  6707  mulidnq  7458  recexnq  7459  ltexnqq  7477  archnqq  7486  prarloclemarch2  7488  addnq0mo  7516  mulnq0mo  7517  addnnnq0  7518  mulnnnq0  7519  nqnq0a  7523  nqnq0m  7524  nq0a0  7526  nnanq0  7527  distrnq0  7528  mulcomnq0  7529  addassnq0  7531  addpinq1  7533  nq02m  7534  prarloclemlo  7563  prarloclem3  7566  prarloclem5  7569  caucvgprlemnkj  7735  caucvgprlemnbj  7736  caucvgprlemm  7737  caucvgprlemdisj  7743  caucvgprlemloc  7744  caucvgprlemcl  7745  caucvgprlemladdfu  7746  caucvgprlemladdrl  7747  caucvgprlem1  7748  caucvgprlem2  7749  caucvgpr  7751  caucvgprprlemell  7754  caucvgprprlemelu  7755  caucvgprprlemcbv  7756  caucvgprprlemval  7757  caucvgprprlemnkeqj  7759  caucvgprprlemmu  7764  caucvgprprlemopl  7766  caucvgprprlemlol  7767  caucvgprprlemopu  7768  caucvgprprlemloc  7772  caucvgprprlemclphr  7774  caucvgprprlemexbt  7775  caucvgprprlem1  7778  caucvgprprlem2  7779  addsrmo  7812  mulsrmo  7813  addsrpr  7814  mulsrpr  7815  prsrriota  7857  caucvgsrlemfv  7860  caucvgsr  7871  suplocsrlemb  7875  suplocsrlempr  7876  suplocsrlem  7877  suplocsr  7878  pitonnlem2  7916  pitonn  7917  nntopi  7963  axcaucvglemval  7966  qus0  13375  qusinv  13376  qussub  13377  quscrng  14099