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

Theorem eleqtri 2697
Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)
Hypotheses
Ref Expression
eleqtr.1 𝐴𝐵
eleqtr.2 𝐵 = 𝐶
Assertion
Ref Expression
eleqtri 𝐴𝐶

Proof of Theorem eleqtri
StepHypRef Expression
1 eleqtr.1 . 2 𝐴𝐵
2 eleqtr.2 . . 3 𝐵 = 𝐶
32eleq2i 2691 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 220 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  wcel 1988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-clel 2616
This theorem is referenced by:  eleqtrri  2698  3eltr3i  2711  prid2  4289  2eluzge0  11718  fz0to4untppr  12426  seqp1i  12800  faclbnd4lem1  13063  cats1fv  13585  bpoly2  14769  bpoly3  14770  bpoly4  14771  ef0lem  14790  phi1  15459  gsumws1  17357  lt6abl  18277  uvcvvcl  20107  smadiadetlem4  20456  indiscld  20876  cnrehmeo  22733  ovolicc1  23265  dvcjbr  23693  vieta1lem2  24047  dvloglem  24375  logdmopn  24376  efopnlem2  24384  cxpcn  24467  loglesqrt  24480  log2ublem2  24655  efrlim  24677  tgcgr4  25407  axlowdimlem16  25818  axlowdimlem17  25819  nlelchi  28890  hmopidmchi  28980  raddcn  29949  xrge0tmd  29966  indf  30051  ballotlem1ri  30570  chtvalz  30681  circlemethhgt  30695  dvtanlem  33430  ftc1cnnc  33455  dvasin  33467  dvacos  33468  dvreasin  33469  dvreacos  33470  areacirclem2  33472  areacirclem4  33474  cncfres  33535  jm2.23  37382  fvnonrel  37722  frege54cor1c  38029  fourierdlem28  40115  fourierdlem57  40143  fourierdlem59  40145  fourierdlem62  40148  fourierdlem68  40154  fouriersw  40211  etransclem23  40237  etransclem35  40249  etransclem38  40252  etransclem39  40253  etransclem44  40258  etransclem45  40259  etransclem47  40261  rrxtopn0  40276  hoidmvlelem2  40573  vonicclem2  40661  fmtno4prmfac  41249
  Copyright terms: Public domain W3C validator