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

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

Proof of Theorem eleqtri
StepHypRef Expression
1 eleqtri.1 . 2 𝐴𝐵
2 eleqtri.2 . . 3 𝐵 = 𝐶
32eleq2i 2909 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 231 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wcel 2107
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 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-clel 2898
This theorem is referenced by:  eleqtrri  2917  3eltr3i  2930  prid2  4698  2eluzge0  12282  fz0to4untppr  13000  seqp1i  13376  faclbnd4lem1  13643  cats1fv  14211  bpoly2  15401  bpoly3  15402  bpoly4  15403  ef0lem  15422  phi1  16100  gsumws1  17985  lt6abl  18935  uvcvvcl  20847  smadiadetlem4  21194  indiscld  21615  cnrehmeo  23472  ovolicc1  24032  dvcjbr  24461  vieta1lem2  24815  dvloglem  25144  logdmopn  25145  efopnlem2  25153  cxpcn  25239  loglesqrt  25252  log2ublem2  25439  efrlim  25461  tgcgr4  26231  axlowdimlem16  26657  axlowdimlem17  26658  nlelchi  29752  hmopidmchi  29842  raddcn  31058  xrge0tmd  31074  indf  31160  ballotlem1ri  31678  chtvalz  31786  circlemethhgt  31800  dvtanlem  34808  ftc1cnnc  34833  dvasin  34845  dvacos  34846  dvreasin  34847  dvreacos  34848  areacirclem2  34850  areacirclem4  34852  cncfres  34911  jm2.23  39458  fvnonrel  39822  frege54cor1c  40126  fourierdlem28  42286  fourierdlem57  42314  fourierdlem59  42316  fourierdlem62  42319  fourierdlem68  42325  fouriersw  42382  etransclem23  42408  etransclem35  42420  etransclem38  42423  etransclem39  42424  etransclem44  42429  etransclem45  42430  etransclem47  42432  rrxtopn0  42444  hoidmvlelem2  42744  vonicclem2  42832  fmtno4prmfac  43566
  Copyright terms: Public domain W3C validator