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

Theorem eceq1d 8315
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 8314 . 2 (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
31, 2syl 17 1 (𝜑 → [𝐴]𝐶 = [𝐵]𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  [cec 8274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529  df-cnv 5531  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-ec 8278
This theorem is referenced by:  brecop  8377  eroveu  8379  erov  8381  ecovcom  8390  ecovass  8391  ecovdi  8392  addsrmo  10488  mulsrmo  10489  addsrpr  10490  mulsrpr  10491  supsrlem  10526  supsr  10527  qus0  18334  qusinv  18335  qussub  18336  sylow2blem2  18742  frgpadd  18885  vrgpval  18889  vrgpinv  18891  frgpup3lem  18899  qusabl  18982  quscrng  20010  qustgplem  22730  pi1addval  23657  pi1xfrf  23662  pi1xfrval  23663  pi1xfrcnvlem  23665  pi1xfrcnv  23666  pi1cof  23668  pi1coval  23669  pi1coghm  23670  vitalilem3  24218  ismntoplly  31380  linedegen  33718  fvline  33719
  Copyright terms: Public domain W3C validator