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

Theorem coeq2 5814
Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)
Assertion
Ref Expression
coeq2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem coeq2
StepHypRef Expression
1 coss2 5812 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 coss2 5812 . . 3 (𝐵𝐴 → (𝐶𝐵) ⊆ (𝐶𝐴))
31, 2anim12i 613 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
4 eqss 3959 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3959 . 2 ((𝐶𝐴) = (𝐶𝐵) ↔ ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
63, 4, 53imtr4i 291 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wss 3910  ccom 5637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-in 3917  df-ss 3927  df-br 5106  df-opab 5168  df-co 5642
This theorem is referenced by:  coeq2i  5816  coeq2d  5818  coi2  6215  f1eqcocnv  7246  f1eqcocnvOLD  7247  ereq1  8654  dfttrcl2  9659  seqf1olem2  13947  seqf1o  13948  relexpsucnnr  14909  isps  18456  pwsco2mhm  18642  gsumwmhm  18654  frmdgsum  18671  frmdup1  18673  frmdup2  18674  efmndov  18690  symggrplem  18693  smndex1mndlem  18718  smndex1mnd  18719  pmtr3ncom  19255  psgnunilem1  19273  frgpuplem  19552  frgpupf  19553  frgpupval  19554  gsumval3eu  19679  gsumval3lem2  19681  selvval  21526  kgencn2  22906  upxp  22972  uptx  22974  txcn  22975  xkococnlem  23008  xkococn  23009  cnmptk1  23030  cnmptkk  23032  xkofvcn  23033  imasdsf1olem  23724  pi1cof  24420  pi1coval  24421  elovolmr  24838  ovoliunlem3  24866  ismbf1  24986  motplusg  27431  hocsubdir  30674  hoddi  30879  lnopco0i  30893  opsqrlem1  31029  pjsdi2i  31046  pjin2i  31082  pjclem1  31084  symgfcoeu  31877  eulerpartgbij  32912  cvmliftmo  33818  cvmliftlem14  33831  cvmliftiota  33835  cvmlift2lem13  33849  cvmlift2  33850  cvmliftphtlem  33851  cvmlift3lem2  33854  cvmlift3lem6  33858  cvmlift3lem7  33859  cvmlift3lem9  33861  cvmlift3  33862  msubco  34065  ftc1anclem8  36148  upixp  36178  coideq  36694  xrneq1  36829  xrneq2  36832  trlcoat  39176  trljco  39193  tgrpov  39201  tendovalco  39218  erngmul  39259  erngmul-rN  39267  dvamulr  39465  dvavadd  39468  dvhmulr  39539  dihjatcclem4  39874  rhmmpl  40720  mendmulr  41492  hoiprodcl2  44767  ovnlecvr  44770  ovncvrrp  44776  ovnsubaddlem2  44783  ovncvr2  44823  opnvonmbllem1  44844  opnvonmbl  44846  ovolval4lem2  44862  ovolval5lem2  44865  ovolval5lem3  44866  ovolval5  44867  ovnovollem2  44869  rngcinv  46250  rngcinvALTV  46262  ringcinv  46301  ringcinvALTV  46325  itcoval1  46720  itcoval2  46721  itcoval3  46722  itcovalsucov  46725
  Copyright terms: Public domain W3C validator