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

Theorem coeq2i 5871
Description: Equality inference for composition of two classes. (Contributed by NM, 16-Nov-2000.)
Hypothesis
Ref Expression
coeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
coeq2i (𝐶𝐴) = (𝐶𝐵)

Proof of Theorem coeq2i
StepHypRef Expression
1 coeq1i.1 . 2 𝐴 = 𝐵
2 coeq2 5869 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  ccom 5689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-co 5694
This theorem is referenced by:  coeq12i  5874  cocnvcnv2  6278  co01  6281  dfpo2  6316  fcoi1  6782  f1ofvswap  7326  dftpos2  8268  tposco  8282  cottrcl  9759  canthp1  10694  cats1co  14895  isoval  17809  mvdco  19463  evlsval  22110  evl1fval1lem  22334  evl1var  22340  pf1ind  22359  rhmply1vr1  22391  rhmply1vsca  22392  imasdsf1olem  24383  hoico1  31775  hoid1i  31808  pjclem1  32214  pjclem3  32216  pjci  32219  cycpmconjv  33162  cycpmconjs  33176  poimirlem9  37636  cdlemk45  40949  cononrel1  43607  trclubgNEW  43631  trclrelexplem  43724  relexpaddss  43731  cotrcltrcl  43738  cortrcltrcl  43753  corclrtrcl  43754  cotrclrcl  43755  cortrclrcl  43756  cotrclrtrcl  43757  cortrclrtrcl  43758  brco3f1o  44046  clsneibex  44115  neicvgbex  44125  subsaliuncl  46373  meadjiun  46481  fundcmpsurinjimaid  47398  dftpos5  48774  tposrescnv  48779
  Copyright terms: Public domain W3C validator