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

Theorem eceq1 6696
Description: Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)
Assertion
Ref Expression
eceq1  |-  ( A  =  B  ->  [ A ] C  =  [ B ] C )

Proof of Theorem eceq1
StepHypRef Expression
1 sneq 3651 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21imaeq2d 5012 . 2  |-  ( A  =  B  ->  ( C " { A }
)  =  ( C
" { B }
) )
3 df-ec 6662 . 2  |-  [ A ] C  =  ( C " { A }
)
4 df-ec 6662 . 2  |-  [ B ] C  =  ( C " { B }
)
52, 3, 43eqtr4g 2340 1  |-  ( A  =  B  ->  [ A ] C  =  [ B ] C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   {csn 3640   "cima 4692   [cec 6658
This theorem is referenced by:  ecelqsg  6714  snec  6722  qliftfun  6743  qliftfuns  6745  qliftval  6747  ecoptocl  6748  brecop  6751  eroveu  6753  erov  6755  th3qlem1  6764  th3qlem2  6765  th3q  6767  ovec  6768  ecovcom  6769  ecovass  6770  ecovdi  6771  supsrlem  8733  supsr  8734  divsfval  13449  divs0  14675  divsinv  14676  divssub  14677  divsghm  14719  sylow1lem3  14911  sylow2blem2  14932  efgi2  15034  frgpadd  15072  vrgpval  15076  vrgpinv  15078  frgpup3lem  15086  divsabl  15157  divscrng  15992  znzrhval  16500  divstgpopn  17802  divstgplem  17803  elpi1i  18544  pi1addval  18546  pi1xfrf  18551  pi1xfrval  18552  pi1xfrcnvlem  18554  pi1xfrcnv  18555  pi1cof  18557  pi1coval  18558  pi1coghm  18559  vitalilem3  18965  linedegen  24766  fvline  24767  pdiveql  26168  prtlem9  26732  prtlem11  26734
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-ec 6662
  Copyright terms: Public domain W3C validator