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

Theorem eceq1d 7366
Description: Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.)
Hypothesis
Ref Expression
eceq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eceq1d  |-  ( ph  ->  [ A ] C  =  [ B ] C
)

Proof of Theorem eceq1d
StepHypRef Expression
1 eceq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eceq1 7365 . 2  |-  ( A  =  B  ->  [ A ] C  =  [ B ] C )
31, 2syl 16 1  |-  ( ph  ->  [ A ] C  =  [ B ] C
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1395   [cec 7327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-opab 4516  df-xp 5014  df-cnv 5016  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-ec 7331
This theorem is referenced by:  brecop  7422  eroveu  7424  erov  7426  ecovcom  7435  ecovass  7436  ecovdi  7437  addsrmo  9467  mulsrmo  9468  addsrpr  9469  mulsrpr  9470  supsrlem  9505  supsr  9506  qus0  16386  qusinv  16387  qussub  16388  sylow2blem2  16768  frgpadd  16908  vrgpval  16912  vrgpinv  16914  frgpup3lem  16922  qusabl  16998  quscrng  18015  qustgplem  20745  pi1addval  21674  pi1xfrf  21679  pi1xfrval  21680  pi1xfrcnvlem  21682  pi1xfrcnv  21683  pi1cof  21685  pi1coval  21686  pi1coghm  21687  vitalilem3  22145  ismntoplly  28164  linedegen  29998  fvline  29999
  Copyright terms: Public domain W3C validator