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

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

Proof of Theorem eceq1
StepHypRef Expression
1 sneq 4637 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
21imaeq2d 6057 . 2 (𝐴 = 𝐵 → (𝐶 “ {𝐴}) = (𝐶 “ {𝐵}))
3 df-ec 8701 . 2 [𝐴]𝐶 = (𝐶 “ {𝐴})
4 df-ec 8701 . 2 [𝐵]𝐶 = (𝐶 “ {𝐵})
52, 3, 43eqtr4g 2797 1 (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  {csn 4627  cima 5678  [cec 8697
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ec 8701
This theorem is referenced by:  eceq1d  8738  ecelqsg  8762  snec  8770  qliftfun  8792  qliftfuns  8794  qliftval  8796  ecoptocl  8797  eroveu  8802  erov  8804  divsfval  17489  qusghm  19123  sylow1lem3  19462  efgi2  19587  frgpup3lem  19639  znzrhval  21093  qustgpopn  23615  qustgplem  23616  elpi1i  24553  pi1xfrf  24560  pi1xfrval  24561  pi1xfrcnvlem  24563  pi1cof  24566  pi1coval  24567  vitalilem3  25118  tgjustr  27714  qusker  32452  qusvscpbl  32454  qusvsval  32455  eceq1i  37132  disjressuc2  37246  disjlem14  37656  prtlem9  37722  prtlem11  37724  rngqiprngimfv  46763  rngqiprngimf1  46765  rngqiprngimfo  46766
  Copyright terms: Public domain W3C validator