Theorem eceq1d 6743

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

Syntax hints:   → wi 4   = wceq 1397  [cec 6705

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203  df-in 3205  df-ss 3212  df-sn 3676  df-pr 3677  df-op 3679  df-br 4090  df-opab 4152  df-xp 4733  df-cnv 4735  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-ec 6709

This theorem is referenced by:  brecop  6799  eroveu  6800  th3qlem1  6811  th3qlem2  6812  th3q  6814  oviec  6815  ecovcom  6816  ecovicom  6817  ecovass  6818  ecoviass  6819  ecovdi  6820  ecovidi  6821  mulidnq  7614  recexnq  7615  ltexnqq  7633  archnqq  7642  prarloclemarch2  7644  addnq0mo  7672  mulnq0mo  7673  addnnnq0  7674  mulnnnq0  7675  nqnq0a  7679  nqnq0m  7680  nq0a0  7682  nnanq0  7683  distrnq0  7684  mulcomnq0  7685  addassnq0  7687  addpinq1  7689  nq02m  7690  prarloclemlo  7719  prarloclem3  7722  prarloclem5  7725  caucvgprlemnkj  7891  caucvgprlemnbj  7892  caucvgprlemm  7893  caucvgprlemdisj  7899  caucvgprlemloc  7900  caucvgprlemcl  7901  caucvgprlemladdfu  7902  caucvgprlemladdrl  7903  caucvgprlem1  7904  caucvgprlem2  7905  caucvgpr  7907  caucvgprprlemell  7910  caucvgprprlemelu  7911  caucvgprprlemcbv  7912  caucvgprprlemval  7913  caucvgprprlemnkeqj  7915  caucvgprprlemmu  7920  caucvgprprlemopl  7922  caucvgprprlemlol  7923  caucvgprprlemopu  7924  caucvgprprlemloc  7928  caucvgprprlemclphr  7930  caucvgprprlemexbt  7931  caucvgprprlem1  7934  caucvgprprlem2  7935  addsrmo  7968  mulsrmo  7969  addsrpr  7970  mulsrpr  7971  prsrriota  8013  caucvgsrlemfv  8016  caucvgsr  8027  suplocsrlemb  8031  suplocsrlempr  8032  suplocsrlem  8033  suplocsr  8034  pitonnlem2  8072  pitonn  8073  nntopi  8119  axcaucvglemval  8122  qus0  13845  qusinv  13846  qussub  13847  quscrng  14571