Theorem eceq1d 6724

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

Syntax hints:   → wi 4   = wceq 1395  [cec 6686

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084  df-opab 4146  df-xp 4725  df-cnv 4727  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-ec 6690

This theorem is referenced by:  brecop  6780  eroveu  6781  th3qlem1  6792  th3qlem2  6793  th3q  6795  oviec  6796  ecovcom  6797  ecovicom  6798  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  mulidnq  7584  recexnq  7585  ltexnqq  7603  archnqq  7612  prarloclemarch2  7614  addnq0mo  7642  mulnq0mo  7643  addnnnq0  7644  mulnnnq0  7645  nqnq0a  7649  nqnq0m  7650  nq0a0  7652  nnanq0  7653  distrnq0  7654  mulcomnq0  7655  addassnq0  7657  addpinq1  7659  nq02m  7660  prarloclemlo  7689  prarloclem3  7692  prarloclem5  7695  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemm  7863  caucvgprlemdisj  7869  caucvgprlemloc  7870  caucvgprlemcl  7871  caucvgprlemladdfu  7872  caucvgprlemladdrl  7873  caucvgprlem1  7874  caucvgprlem2  7875  caucvgpr  7877  caucvgprprlemell  7880  caucvgprprlemelu  7881  caucvgprprlemcbv  7882  caucvgprprlemval  7883  caucvgprprlemnkeqj  7885  caucvgprprlemmu  7890  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemopu  7894  caucvgprprlemloc  7898  caucvgprprlemclphr  7900  caucvgprprlemexbt  7901  caucvgprprlem1  7904  caucvgprprlem2  7905  addsrmo  7938  mulsrmo  7939  addsrpr  7940  mulsrpr  7941  prsrriota  7983  caucvgsrlemfv  7986  caucvgsr  7997  suplocsrlemb  8001  suplocsrlempr  8002  suplocsrlem  8003  suplocsr  8004  pitonnlem2  8042  pitonn  8043  nntopi  8089  axcaucvglemval  8092  qus0  13780  qusinv  13781  qussub  13782  quscrng  14505