MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eceq1d Structured version   Visualization version   GIF version

Theorem eceq1d 8770
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
StepHypRef Expression
1 eceq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 eceq1 8769 . 2 (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
31, 2syl 17 1 (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  [cec 8729
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5688  df-cnv 5690  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ec 8733
This theorem is referenced by:  brecop  8835  eroveu  8837  erov  8839  ecovcom  8848  ecovass  8849  ecovdi  8850  addsrmo  11104  mulsrmo  11105  addsrpr  11106  mulsrpr  11107  supsrlem  11142  supsr  11143  qus0  19151  qusinv  19152  qussub  19153  sylow2blem2  19583  frgpadd  19725  vrgpval  19729  vrgpinv  19731  frgpup3lem  19739  qusabl  19827  quscrng  21182  pzriprnglem11  21424  pzriprnglem12  21425  qustgplem  24045  pi1addval  24995  pi1xfrf  25000  pi1xfrval  25001  pi1xfrcnvlem  25003  pi1xfrcnv  25004  pi1cof  25006  pi1coval  25007  pi1coghm  25008  vitalilem3  25559  elrlocbasi  33005  rlocaddval  33007  rlocmulval  33008  rloccring  33009  rloc0g  33010  rloc1r  33011  rlocf1  33012  idomsubr  33020  opprqusmulr  33227  zringfrac  33277  ismntoplly  33659  linedegen  35772  fvline  35773
  Copyright terms: Public domain W3C validator