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

Theorem eceq1 6933
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 3817 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21imaeq2d 5195 . 2  |-  ( A  =  B  ->  ( C " { A }
)  =  ( C
" { B }
) )
3 df-ec 6899 . 2  |-  [ A ] C  =  ( C " { A }
)
4 df-ec 6899 . 2  |-  [ B ] C  =  ( C " { B }
)
52, 3, 43eqtr4g 2492 1  |-  ( A  =  B  ->  [ A ] C  =  [ B ] C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   {csn 3806   "cima 4873   [cec 6895
This theorem is referenced by:  ecelqsg  6951  snec  6959  qliftfun  6981  qliftfuns  6983  qliftval  6985  ecoptocl  6986  brecop  6989  eroveu  6991  erov  6993  th3qlem1  7002  th3qlem2  7003  th3q  7005  ovec  7006  ecovcom  7007  ecovass  7008  ecovdi  7009  supsrlem  8978  supsr  8979  divsfval  13764  divs0  14990  divsinv  14991  divssub  14992  divsghm  15034  sylow1lem3  15226  sylow2blem2  15247  efgi2  15349  frgpadd  15387  vrgpval  15391  vrgpinv  15393  frgpup3lem  15401  divsabl  15472  divscrng  16303  znzrhval  16819  divstgpopn  18141  divstgplem  18142  elpi1i  19063  pi1addval  19065  pi1xfrf  19070  pi1xfrval  19071  pi1xfrcnvlem  19073  pi1xfrcnv  19074  pi1cof  19076  pi1coval  19077  pi1coghm  19078  vitalilem3  19494  linedegen  26069  fvline  26070  prtlem9  26704  prtlem11  26706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-xp 4876  df-cnv 4878  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-ec 6899
  Copyright terms: Public domain W3C validator