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

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

Proof of Theorem eceq1
StepHypRef Expression
1 sneq 4574 . . 3 (𝐴 = 𝐵 → {𝐴} = {𝐵})
21imaeq2d 5927 . 2 (𝐴 = 𝐵 → (𝐶 “ {𝐴}) = (𝐶 “ {𝐵}))
3 df-ec 8281 . 2 [𝐴]𝐶 = (𝐶 “ {𝐴})
4 df-ec 8281 . 2 [𝐵]𝐶 = (𝐶 “ {𝐵})
52, 3, 43eqtr4g 2886 1 (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  {csn 4564  cima 5557  [cec 8277
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-xp 5560  df-cnv 5562  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-ec 8281
This theorem is referenced by:  eceq1d  8318  ecelqsg  8342  snec  8350  qliftfun  8372  qliftfuns  8374  qliftval  8376  ecoptocl  8377  eroveu  8382  erov  8384  divsfval  16810  qusghm  18325  sylow1lem3  18645  efgi2  18771  frgpup3lem  18823  znzrhval  20612  qustgpopn  22646  qustgplem  22647  elpi1i  23568  pi1xfrf  23575  pi1xfrval  23576  pi1xfrcnvlem  23578  pi1cof  23581  pi1coval  23582  vitalilem3  24129  tgjustr  26177  qusker  30835  qusvscpbl  30837  qusscaval  30838  eceq1i  35404  prtlem9  35870  prtlem11  35872
  Copyright terms: Public domain W3C validator