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

Theorem coeq1i 5420
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 5418 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  ccom 5253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-in 3730  df-ss 3737  df-br 4787  df-opab 4847  df-co 5258
This theorem is referenced by:  coeq12i  5424  cocnvcnv1  5790  hashgval  13324  imasdsval2  16384  prds1  18822  pf1mpf  19931  upxp  21647  uptx  21649  hoico2  28956  hoid1ri  28989  nmopcoadj2i  29301  pjclem3  29396  erdsze2lem2  31524  pprodcnveq  32327  diblss  36980  cononrel2  38427  trclubgNEW  38451  cortrcltrcl  38558  corclrtrcl  38559  cortrclrcl  38561  cotrclrtrcl  38562  cortrclrtrcl  38563  neicvgbex  38936  neicvgnvo  38939  dvsinax  40645
  Copyright terms: Public domain W3C validator