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

Theorem coeq2i 5282
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 5280 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴) = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1483  ccom 5118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588  df-br 4654  df-opab 4713  df-co 5123
This theorem is referenced by:  coeq12i  5285  cocnvcnv2  5647  co01  5650  fcoi1  6078  dftpos2  7369  tposco  7383  canthp1  9476  cats1co  13601  isoval  16425  mvdco  17865  evlsval  19519  evl1fval1lem  19694  evl1var  19700  pf1ind  19719  imasdsf1olem  22178  hoico1  28615  hoid1i  28648  pjclem1  29054  pjclem3  29056  pjci  29059  dfpo2  31645  poimirlem9  33418  cdlemk45  36235  cononrel1  37900  trclubgNEW  37925  trclrelexplem  38003  relexpaddss  38010  cotrcltrcl  38017  cortrcltrcl  38032  corclrtrcl  38033  cotrclrcl  38034  cortrclrcl  38035  cotrclrtrcl  38036  cortrclrtrcl  38037  brco3f1o  38331  clsneibex  38400  neicvgbex  38410  subsaliuncl  40576  meadjiun  40683
  Copyright terms: Public domain W3C validator