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

Theorem eleqtri 2680
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 2674 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 218 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2597  df-clel 2600
This theorem is referenced by:  eleqtrri  2681  3eltr3i  2694  prid2  4236  2eluzge0  11560  fz0to4untppr  12261  seqp1i  12629  faclbnd4lem1  12892  cats1fv  13396  bpoly2  14568  bpoly3  14569  bpoly4  14570  ef0lem  14589  phi1  15257  gsumws1  17140  lt6abl  18060  uvcvvcl  19882  smadiadetlem4  20231  indiscld  20642  cnrehmeo  22486  ovolicc1  23003  dvcjbr  23430  vieta1lem2  23782  dvloglem  24106  logdmopn  24107  efopnlem2  24115  cxpcn  24198  loglesqrt  24211  log2ublem2  24386  efrlim  24408  tgcgr4  25139  axlowdimlem16  25550  axlowdimlem17  25551  konigsberg  26275  nlelchi  28105  hmopidmchi  28195  raddcn  29104  xrge0tmd  29121  indf  29206  ballotlem1ri  29724  dvtanlem  32427  ftc1cnnc  32452  dvasin  32464  dvacos  32465  dvreasin  32466  dvreacos  32467  areacirclem2  32469  areacirclem4  32471  cncfres  32532  jm2.23  36379  fvnonrel  36720  frege54cor1c  37027  fourierdlem28  38827  fourierdlem57  38855  fourierdlem59  38857  fourierdlem62  38860  fourierdlem68  38866  fouriersw  38923  etransclem23  38949  etransclem35  38961  etransclem38  38964  etransclem39  38965  etransclem44  38970  etransclem45  38971  etransclem47  38973  rrxtopn0  38988  hoidmvlelem2  39285  vonicclem2  39374  fmtno4prmfac  39822
  Copyright terms: Public domain W3C validator