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

Theorem coeq1i 5728
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 5726 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  ccom 5557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-in 3946  df-ss 3955  df-br 5063  df-opab 5125  df-co 5562
This theorem is referenced by:  coeq12i  5732  cocnvcnv1  6107  hashgval  13686  imasdsval2  16781  prds1  19286  pf1mpf  20431  upxp  22147  uptx  22149  hoico2  29449  hoid1ri  29482  nmopcoadj2i  29794  pjclem3  29889  cycpmconjslem1  30711  cycpmconjs  30713  cyc3conja  30714  erdsze2lem2  32336  pprodcnveq  33229  diblss  38174  cononrel2  39817  trclubgNEW  39840  cortrcltrcl  39947  corclrtrcl  39948  cortrclrcl  39950  cotrclrtrcl  39951  cortrclrtrcl  39952  neicvgbex  40324  neicvgnvo  40327  dvsinax  42059
  Copyright terms: Public domain W3C validator