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

Theorem eceq1 8784
Description: Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
Assertion
Ref Expression
eceq1 (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)

Proof of Theorem eceq1
StepHypRef Expression
1 sneq 4636 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
21imaeq2d 6078 . 2 (𝐴 = 𝐵 → (𝐶 “ {𝐴}) = (𝐶 “ {𝐵}))
3 df-ec 8747 . 2 [𝐴]𝐶 = (𝐶 “ {𝐴})
4 df-ec 8747 . 2 [𝐵]𝐶 = (𝐶 “ {𝐵})
52, 3, 43eqtr4g 2802 1 (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  {csn 4626  cima 5688  [cec 8743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ec 8747
This theorem is referenced by:  eceq1d  8785  ecelqsg  8812  snec  8820  qliftfun  8842  qliftfuns  8844  qliftval  8846  ecoptocl  8847  eroveu  8852  erov  8854  divsfval  17592  qusghm  19273  sylow1lem3  19618  efgi2  19743  frgpup3lem  19795  rngqiprngimfv  21308  rngqiprngimf1  21310  rngqiprngimfo  21311  pzriprnglem11  21502  znzrhval  21565  qustgpopn  24128  qustgplem  24129  elpi1i  25079  pi1xfrf  25086  pi1xfrval  25087  pi1xfrcnvlem  25089  pi1cof  25092  pi1coval  25093  vitalilem3  25645  tgjustr  28482  qusker  33377  qusvscpbl  33379  qusvsval  33380  algextdeg  33766  eceq1i  38277  disjressuc2  38389  disjlem14  38799  prtlem9  38865  prtlem11  38867  aks6d1c6lem5  42178  aks5lem3a  42190
  Copyright terms: Public domain W3C validator