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

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

Proof of Theorem coeq1i
StepHypRef Expression
1 coeq1i.1 . 2 𝐴 = 𝐵
2 coeq1 5868 . 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  cocnvcnv1  6277  ttrclco  9758  hashgval  14372  imasdsval2  17561  prds1  20320  pf1mpf  22356  upxp  23631  uptx  23633  hoico2  31776  hoid1ri  31809  nmopcoadj2i  32121  pjclem3  32216  cycpmconjslem1  33174  cycpmconjs  33176  cyc3conja  33177  1arithidomlem2  33564  erdsze2lem2  35209  pprodcnveq  35884  diblss  41172  cononrel2  43608  trclubgNEW  43631  cortrcltrcl  43753  corclrtrcl  43754  cortrclrcl  43756  cotrclrtrcl  43757  cortrclrtrcl  43758  neicvgbex  44125  neicvgnvo  44128  dvsinax  45928
  Copyright terms: Public domain W3C validator