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

Theorem eceq1d 7355
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 7354 . 2  |-  ( A  =  B  ->  [ A ] C  =  [ B ] C )
31, 2syl 17 1  |-  ( ph  ->  [ A ] C  =  [ B ] C
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   [cec 7316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-br 4367  df-opab 4426  df-xp 4802  df-cnv 4804  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-ec 7320
This theorem is referenced by:  brecop  7411  eroveu  7413  erov  7415  ecovcom  7424  ecovass  7425  ecovdi  7426  addsrmo  9448  mulsrmo  9449  addsrpr  9450  mulsrpr  9451  supsrlem  9486  supsr  9487  qus0  16818  qusinv  16819  qussub  16820  sylow2blem2  17216  frgpadd  17356  vrgpval  17360  vrgpinv  17362  frgpup3lem  17370  qusabl  17446  quscrng  18407  qustgplem  21077  pi1addval  22021  pi1xfrf  22026  pi1xfrval  22027  pi1xfrcnvlem  22029  pi1xfrcnv  22030  pi1cof  22032  pi1coval  22033  pi1coghm  22034  vitalilem3  22510  ismntoplly  28781  linedegen  30859  fvline  30860
  Copyright terms: Public domain W3C validator