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

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

Proof of Theorem eceq1
StepHypRef Expression
1 sneq 4178 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
21imaeq2d 5454 . 2 (𝐴 = 𝐵 → (𝐶 “ {𝐴}) = (𝐶 “ {𝐵}))
3 df-ec 7729 . 2 [𝐴]𝐶 = (𝐶 “ {𝐴})
4 df-ec 7729 . 2 [𝐵]𝐶 = (𝐶 “ {𝐵})
52, 3, 43eqtr4g 2679 1 (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  {csn 4168  cima 5107  [cec 7725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110  df-cnv 5112  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-ec 7729
This theorem is referenced by:  eceq1d  7768  ecelqsg  7787  snec  7795  qliftfun  7817  qliftfuns  7819  qliftval  7821  ecoptocl  7822  eroveu  7827  erov  7829  divsfval  16188  qusghm  17678  sylow1lem3  17996  efgi2  18119  frgpup3lem  18171  znzrhval  19876  qustgpopn  21904  qustgplem  21905  elpi1i  22827  pi1xfrf  22834  pi1xfrval  22835  pi1xfrcnvlem  22837  pi1cof  22840  pi1coval  22841  vitalilem3  23360  prtlem9  33968  prtlem11  33970
  Copyright terms: Public domain W3C validator