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

Theorem coeq2i 5191
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 5189 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  ccom 5031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-in 3546  df-ss 3553  df-br 4578  df-opab 4638  df-co 5036
This theorem is referenced by:  coeq12i  5194  cocnvcnv2  5549  co01  5552  fcoi1  5975  dftpos2  7233  tposco  7247  canthp1  9332  cats1co  13400  isoval  16196  mvdco  17636  evlsval  19288  evl1fval1lem  19463  evl1var  19469  pf1ind  19488  imasdsf1olem  21935  hoico1  27792  hoid1i  27825  pjclem1  28231  pjclem3  28233  pjci  28236  dfpo2  30691  poimirlem9  32371  cdlemk45  35036  cononrel1  36702  trclubgNEW  36727  trclrelexplem  36805  relexpaddss  36812  cotrcltrcl  36819  cortrcltrcl  36834  corclrtrcl  36835  cotrclrcl  36836  cortrclrcl  36837  cotrclrtrcl  36838  cortrclrtrcl  36839  brco3f1o  37134  clsneibex  37203  neicvgbex  37213  subsaliuncl  39035  meadjiun  39142
  Copyright terms: Public domain W3C validator