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

Theorem eleqtri 2540
Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)
Hypotheses
Ref Expression
eleqtr.1  |-  A  e.  B
eleqtr.2  |-  B  =  C
Assertion
Ref Expression
eleqtri  |-  A  e.  C

Proof of Theorem eleqtri
StepHypRef Expression
1 eleqtr.1 . 2  |-  A  e.  B
2 eleqtr.2 . . 3  |-  B  =  C
32eleq2i 2532 . 2  |-  ( A  e.  B  <->  A  e.  C )
41, 3mpbi 208 1  |-  A  e.  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    e. wcel 1823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-cleq 2446  df-clel 2449
This theorem is referenced by:  eleqtrri  2541  3eltr3i  2554  prid2  4125  2eluzge0  11126  seqp1i  12108  faclbnd4lem1  12356  cats1fv  12818  ef0lem  13899  phi1  14390  gsumws1  16209  lt6abl  17099  uvcvvcl  18992  smadiadetlem4  19341  indiscld  19762  cnrehmeo  21622  ovolicc1  22096  dvcjbr  22521  vieta1lem2  22876  dvloglem  23200  logdmopn  23201  efopnlem2  23209  cxpcn  23290  loglesqrt  23303  log2ublem2  23478  efrlim  23500  axlowdimlem16  24465  axlowdimlem17  24466  usgraexvlem  24600  konigsberg  25192  nlelchi  27181  hmopidmchi  27271  raddcn  28149  xrge0tmd  28166  indf  28248  ballotlem1ri  28740  bpoly2  30050  bpoly3  30051  bpoly4  30052  dvtanlem  30307  ftc1cnnc  30332  dvasin  30346  dvacos  30347  dvreasin  30348  dvreacos  30349  areacirclem2  30351  areacirclem4  30353  cncfres  30504  jm2.23  31180  fourierdlem28  32159  fourierdlem57  32188  fourierdlem59  32190  fourierdlem62  32193  fourierdlem68  32199  fouriersw  32256  etransclem23  32282  etransclem35  32294  etransclem38  32297  etransclem39  32298  etransclem44  32303  etransclem45  32304  etransclem47  32306  frege54cor1c  38416
  Copyright terms: Public domain W3C validator