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

Theorem coeq2 5697
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 5695 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 coss2 5695 . . 3 (𝐵𝐴 → (𝐶𝐵) ⊆ (𝐶𝐴))
31, 2anim12i 615 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
4 eqss 3933 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3933 . 2 ((𝐶𝐴) = (𝐶𝐵) ↔ ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
63, 4, 53imtr4i 295 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wss 3884  ccom 5527
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-br 5034  df-opab 5096  df-co 5532
This theorem is referenced by:  coeq2i  5699  coeq2d  5701  coi2  6087  f1eqcocnv  7039  f1eqcocnvOLD  7040  ereq1  8283  seqf1olem2  13410  seqf1o  13411  relexpsucnnr  14379  isps  17807  pwsco2mhm  17992  gsumwmhm  18005  frmdgsum  18022  frmdup1  18024  frmdup2  18025  efmndov  18041  symggrplem  18044  smndex1mndlem  18069  smndex1mnd  18070  pmtr3ncom  18598  psgnunilem1  18616  frgpuplem  18893  frgpupf  18894  frgpupval  18895  gsumval3eu  19020  gsumval3lem2  19022  selvval  20793  kgencn2  22165  upxp  22231  uptx  22233  txcn  22234  xkococnlem  22267  xkococn  22268  cnmptk1  22289  cnmptkk  22291  xkofvcn  22292  imasdsf1olem  22983  pi1cof  23667  pi1coval  23668  elovolmr  24083  ovoliunlem3  24111  ismbf1  24231  motplusg  26339  hocsubdir  29571  hoddi  29776  lnopco0i  29790  opsqrlem1  29926  pjsdi2i  29943  pjin2i  29979  pjclem1  29981  symgfcoeu  30779  eulerpartgbij  31738  cvmliftmo  32639  cvmliftlem14  32652  cvmliftiota  32656  cvmlift2lem13  32670  cvmlift2  32671  cvmliftphtlem  32672  cvmlift3lem2  32675  cvmlift3lem6  32679  cvmlift3lem7  32680  cvmlift3lem9  32682  cvmlift3  32683  msubco  32886  ftc1anclem8  35130  upixp  35160  coideq  35660  xrneq1  35782  xrneq2  35785  trlcoat  38012  trljco  38029  tgrpov  38037  tendovalco  38054  erngmul  38095  erngmul-rN  38103  dvamulr  38301  dvavadd  38304  dvhmulr  38375  dihjatcclem4  38710  mendmulr  40119  hoiprodcl2  43181  ovnlecvr  43184  ovncvrrp  43190  ovnsubaddlem2  43197  ovncvr2  43237  opnvonmbllem1  43258  opnvonmbl  43260  ovolval4lem2  43276  ovolval5lem2  43279  ovolval5lem3  43280  ovolval5  43281  ovnovollem2  43283  rngcinv  44592  rngcinvALTV  44604  ringcinv  44643  ringcinvALTV  44667  itcoval1  45064  itcoval2  45065  itcoval3  45066  itcovalsucov  45069
  Copyright terms: Public domain W3C validator