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

Theorem eleqtri 2836
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 2829 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 229 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wcel 2106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728  df-clel 2814
This theorem is referenced by:  eleqtrri  2837  3eltr3i  2850  prid2  4724  2eluzge0  12818  fz0to4untppr  13544  faclbnd4lem1  14193  cats1fv  14748  bpoly2  15940  bpoly3  15941  bpoly4  15942  ef0lem  15961  phi1  16645  gsumws1  18648  lt6abl  19672  uvcvvcl  21193  mhpvarcl  21538  smadiadetlem4  22018  indiscld  22442  cnrehmeo  24316  ovolicc1  24880  dvcjbr  25313  vieta1lem2  25671  dvloglem  26003  logdmopn  26004  efopnlem2  26012  cxpcn  26098  loglesqrt  26111  log2ublem2  26297  efrlim  26319  tgcgr4  27473  axlowdimlem16  27906  axlowdimlem17  27907  nlelchi  31003  hmopidmchi  31093  raddcn  32510  xrge0tmd  32526  indf  32614  ballotlem1ri  33134  chtvalz  33242  circlemethhgt  33256  dvtanlem  36127  ftc1cnnc  36150  dvasin  36162  dvacos  36163  dvreasin  36164  dvreacos  36165  areacirclem2  36167  areacirclem4  36169  cncfres  36224  jm2.23  41306  0finon  41710  1finon  41711  2finon  41712  3finon  41713  4finon  41714  fvnonrel  41859  frege54cor1c  42177  fourierdlem28  44366  fourierdlem57  44394  fourierdlem59  44396  fourierdlem62  44399  fourierdlem68  44405  fouriersw  44462  etransclem23  44488  etransclem35  44500  etransclem38  44503  etransclem39  44504  etransclem44  44509  etransclem45  44510  etransclem47  44512  rrxtopn0  44524  hoidmvlelem2  44827  vonicclem2  44915  fmtno4prmfac  45754
  Copyright terms: Public domain W3C validator