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

Theorem coeq1i 5856
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 5854 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  ccom 5678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3953  df-ss 3963  df-br 5147  df-opab 5209  df-co 5683
This theorem is referenced by:  coeq12i  5860  cocnvcnv1  6252  ttrclco  9708  hashgval  14288  imasdsval2  17457  prds1  20125  pf1mpf  21852  upxp  23108  uptx  23110  hoico2  30987  hoid1ri  31020  nmopcoadj2i  31332  pjclem3  31427  cycpmconjslem1  32290  cycpmconjs  32292  cyc3conja  32293  erdsze2lem2  34132  pprodcnveq  34792  diblss  39978  cononrel2  42278  trclubgNEW  42301  cortrcltrcl  42423  corclrtrcl  42424  cortrclrcl  42426  cotrclrtrcl  42427  cortrclrtrcl  42428  neicvgbex  42795  neicvgnvo  42798  dvsinax  44563
  Copyright terms: Public domain W3C validator