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

Theorem coeq2 5451
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 5449 . . 3 (𝐴𝐵 → (𝐶𝐴) ⊆ (𝐶𝐵))
2 coss2 5449 . . 3 (𝐵𝐴 → (𝐶𝐵) ⊆ (𝐶𝐴))
31, 2anim12i 606 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
4 eqss 3778 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
5 eqss 3778 . 2 ((𝐶𝐴) = (𝐶𝐵) ↔ ((𝐶𝐴) ⊆ (𝐶𝐵) ∧ (𝐶𝐵) ⊆ (𝐶𝐴)))
63, 4, 53imtr4i 283 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wss 3734  ccom 5283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-in 3741  df-ss 3748  df-br 4812  df-opab 4874  df-co 5288
This theorem is referenced by:  coeq2i  5453  coeq2d  5455  coi2  5840  relcnvtr  5843  f1eqcocnv  6752  ereq1  7958  seqf1olem2  13053  seqf1o  13054  relexpsucnnr  14064  isps  17482  pwsco2mhm  17651  gsumwmhm  17663  frmdgsum  17680  frmdup1  17682  frmdup2  17683  symgov  18087  pmtr3ncom  18172  psgnunilem1  18190  frgpuplem  18465  frgpupf  18466  frgpupval  18467  gsumval3eu  18585  gsumval3lem2  18587  kgencn2  21654  upxp  21720  uptx  21722  txcn  21723  xkococnlem  21756  xkococn  21757  cnmptk1  21778  cnmptkk  21780  xkofvcn  21781  imasdsf1olem  22471  pi1cof  23151  pi1coval  23152  elovolmr  23548  ovoliunlem3  23576  ismbf1  23696  motplusg  25742  hocsubdir  29121  hoddi  29326  lnopco0i  29340  opsqrlem1  29476  pjsdi2i  29493  pjin2i  29529  pjclem1  29531  symgfcoeu  30313  eulerpartgbij  30902  cvmliftmo  31735  cvmliftlem14  31748  cvmliftiota  31752  cvmlift2lem13  31766  cvmlift2  31767  cvmliftphtlem  31768  cvmlift3lem2  31771  cvmlift3lem6  31775  cvmlift3lem7  31776  cvmlift3lem9  31778  cvmlift3  31779  msubco  31897  ftc1anclem8  33936  upixp  33968  coideq  34466  xrneq1  34589  xrneq2  34592  trlcoat  36700  trljco  36717  tgrpov  36725  tendovalco  36742  erngmul  36783  erngmul-rN  36791  dvamulr  36989  dvavadd  36992  dvhmulr  37063  dihjatcclem4  37398  mendmulr  38459  hoiprodcl2  41433  ovnlecvr  41436  ovncvrrp  41442  ovnsubaddlem2  41449  ovncvr2  41489  opnvonmbllem1  41510  opnvonmbl  41512  ovolval4lem2  41528  ovolval5lem2  41531  ovolval5lem3  41532  ovolval5  41533  ovnovollem2  41535  rngcinv  42674  rngcinvALTV  42686  ringcinv  42725  ringcinvALTV  42749
  Copyright terms: Public domain W3C validator