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

Theorem eleqtri 2507
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-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 2499 . 2  |-  ( A  e.  B  <->  A  e.  C )
41, 3mpbi 200 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eleqtrri  2508  3eltr3i  2513  prid2  3905  seqp1i  11331  faclbnd4lem1  11576  bcn1  11596  bcpasc  11604  cats1fv  11815  ef0lem  12673  phi1  13154  dfphi2  13155  gsumws1  14777  efgsp1  15361  efgsres  15362  efgredlemd  15368  efgredlem  15371  lt6abl  15496  indiscld  17147  cnrehmeo  18970  ovolicc1  19404  iblcnlem1  19671  dvcjbr  19827  c1lip2  19874  dvply1  20193  vieta1lem2  20220  dvtaylp  20278  taylthlem2  20282  dvloglem  20531  logdmopn  20532  efopnlem2  20540  logtayl  20543  cxpcn  20621  loglesqr  20634  leibpilem2  20773  log2ublem2  20779  efrlim  20800  basellem5  20859  ppiltx  20952  prmorcht  20953  chtlepsi  20982  chpub  20996  chebbnd1lem1  21155  chtppilimlem1  21159  usgraexvlem  21406  konigsberg  21701  nlelchi  23556  hmopidmchi  23646  raddcn  24307  xrge0tmd  24324  indf  24405  ballotlemfrci  24777  ballotlemfrceq  24778  ballotlem1ri  24784  axlowdimlem16  25888  axlowdimlem17  25889  axlowdim  25892  bpoly2  26095  bpoly3  26096  bpoly4  26097  ftc1cnnc  26269  areacirclem4  26284  areacirclem5  26286  cncfres  26465  jm2.23  27058  uvcvvcl  27204
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator